Changeset 1528 for src/utilities/binary/division.ma
 Timestamp:
 Nov 22, 2011, 11:58:43 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/binary/division.ma
r1523 r1528 92 92 theorem plus_minus_r: 93 93 ∀m,n,p:Pos. m < n → p+(nm) = (p+n)m. 94 #m #n #p #le >(commutative_plus …)95 >(commutative_plus p ?) @plus_minus //; qed.94 #m #n #p #le >(commutative_plus_pos …) 95 >(commutative_plus_pos p ?) @plus_minus //; qed. 96 96 97 97 lemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+pn≤p. … … 169 169  MinusPos r ⇒ n = m+r 170 170 ]. 171 #n #m lapply (pos_compare_to_Prop n m); lapply (minus_to_plus n m);171 #n #m lapply (pos_compare_to_Prop n m); lapply (minus_to_plus_pos n m); 172 172 normalize; cases (partial_minus n m); /2/; qed. 173 173 … … 275 275 cases md'; [ 2,4: #md'' ] #DIVIDE normalize; 276 276 >DIV in ⊢ (% → ?); #H #lt destruct; 277 [ lapply (plus_to_minus … e0);277 [ lapply (plus_to_minus_pos … e0); 278 278 >(commutative_times …) >(commutative_times dv'' …) 279 279 cut (dv'' < dv); [ cut (dv''*m < dv*m); /2/; ] #dvlt
Note: See TracChangeset
for help on using the changeset viewer.