Changeset 14 for Csemantics/extralib.ma
 Timestamp:
 Jul 21, 2010, 3:08:58 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/extralib.ma
r11 r14 649 649  pos m ⇒ natp_to_Z (snd ?? (divide n m)) 650 650  neg m ⇒ match divide n m with [ mk_pair q r ⇒ 651 match r with [ pzero ⇒ OZ  _ ⇒ y (natp_to_Z r) ] ]651 match r with [ pzero ⇒ OZ  _ ⇒ y+(natp_to_Z r) ] ] 652 652 ] 653 653  neg n ⇒ … … 655 655 [ OZ ⇒ OZ 656 656  pos m ⇒ match divide n m with [ mk_pair q r ⇒ 657 match r with [ pzero ⇒ OZ  _ ⇒ y +(natp_to_Z r) ] ]657 match r with [ pzero ⇒ OZ  _ ⇒ y(natp_to_Z r) ] ] 658 658  neg m ⇒ natp_to_Z (snd ?? (divide n m)) 659 659 ] … … 664 664 interpretation "integer division" 'divide m n = (divZ m n). 665 665 interpretation "integer modulus" 'module m n = (modZ m n). 666 667 nlemma Zminus_Zlt: ∀x,y:Z. y>0 → xy < x. 668 #x y; ncases y; 669 ##[ #H; napply (False_ind … H); 670 ## #m; #_; ncases x; //; #n; 671 nwhd in ⊢ (?%?); 672 nlapply (pos_compare_to_Prop n m); 673 ncases (pos_compare n m); /2/; 674 #lt; nwhd; nrewrite < (minus_Sn_m … lt); /2/; 675 ## #m H; napply (False_ind … H); 676 ##] nqed. 677 678 nlemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT. 679 #n m lt; nlapply (pos_compare_to_Prop n m); ncases (pos_compare n m); 680 ##[ //; 681 ## ##2,3: #H; napply False_ind; napply (absurd ? lt ?); /3/; 682 ##] nqed. 683 684 ntheorem modZ_lt_mod: ∀x,y:Z. y>0 → 0 ≤ x \mod y ∧ x \mod y < y. 685 #x y; ncases y; 686 ##[ #H; napply (False_ind … H); 687 ## #m; #_; ncases x; 688 ##[ @;//; 689 ## #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m)); 690 ncases (divide n m) in ⊢ (???% → %); #dv md H; 691 nelim (divide_ok … H); #e l; nelim l; /2/; 692 ## #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m)); 693 ncases (divide n m) in ⊢ (???% → %); #dv md H; 694 nelim (divide_ok … H); #e l; nelim l; 695 ##[ /2/; 696 ## #md' m' l'; @; 697 ##[ nwhd in ⊢ (??%); nrewrite > (pos_compare_n_m_m_n …); 698 nrewrite > (pos_compare_lt … l'); //; 699 ## /2/; 700 ##] 701 ##] 702 ##] 703 ## #m H; napply (False_ind … H); 704 ##] nqed.
Note: See TracChangeset
for help on using the changeset viewer.