Changeset 15 for Csemantics/extralib.ma
 Timestamp:
 Jul 22, 2010, 4:50:06 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/extralib.ma
r14 r15 119 119 nlemma Zmax_l: ∀x,y. x ≤ Zmax x y. 120 120 #x;#y;nwhd in ⊢ (??%); nlapply (Z_compare_to_Prop x y); ncases (Z_compare x y); 121 /3/; n qed.121 /3/; ncases x; /3/; nqed. 122 122 123 123 nlemma Zmax_r: ∀x,y. y ≤ Zmax x y. 124 124 #x;#y;nwhd in ⊢ (??%); nlapply (Z_compare_to_Prop x y); ncases (Z_compare x y); 125 /3/; #H; nrewrite > H; //; nqed.125 ncases x; /3/; nqed. 126 126 127 127 ntheorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y. … … 169 169 interpretation "integer 'not greater than'" 'ngtr x y = (Not (Zgt x y)). 170 170 171 ndefinition Zleb : Z → Z → bool ≝ 172 λx,y:Z. 171 nlet rec Zleb (x:Z) (y:Z) : bool ≝ 173 172 match x with 174 173 [ OZ ⇒ … … 188 187  neg m ⇒ leb m n ]]. 189 188 190 ndefinition Zltb : Z → Z → bool ≝ 191 λx,y:Z. 189 nlet rec Zltb (x:Z) (y:Z) : bool ≝ 192 190 match x with 193 191 [ OZ ⇒ … … 267 265 ##] nqed. 268 266 269 n definition Z_times : Z → Z →Z ≝270 λx,y.match x with267 nlet rec Z_times (x:Z) (y:Z) : Z ≝ 268 match x with 271 269 [ OZ ⇒ OZ 272 270  pos n ⇒ … … 697 695 ##[ nwhd in ⊢ (??%); nrewrite > (pos_compare_n_m_m_n …); 698 696 nrewrite > (pos_compare_lt … l'); //; 699 ## /2/;697 ## napply Zminus_Zlt; //; 700 698 ##] 701 699 ##]
Note: See TracChangeset
for help on using the changeset viewer.