Module tacdef


Require Export Omega.

Tactic Definition SolveBounds b := 

(Abstract (Try Unfold no_overlap ; Repeat Rewrite two_2;Simpl;Repeat Rewrite <- (plus_sym O);Simpl;

           Repeat Rewrite inj_plus ; Repeat Rewrite inj_minus1 ; Repeat Rewrite inj_minus_div2;

           Generalize (div2_le b);Intros ; Omega)).

Tactic Definition Omega' := Abstract Omega.

Index

This page has been generated by coqdoc