Changeset 1528 for src/utilities
 Timestamp:
 Nov 22, 2011, 11:58:43 AM (9 years ago)
 Location:
 src/utilities/binary
 Files:

 2 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 
src/utilities/binary/positive.ma
r1523 r1528 217 217 ] qed. 218 218 219 theorem commutative_plus : commutative ? plus.219 theorem commutative_plus_pos : commutative ? plus. 220 220 #n elim n; 221 221 [ #y cases y; normalize; //; … … 224 224 225 225 theorem pluss_succn_m: ∀n,m. succ (n + m) = (succ n) + m. 226 #n #m >(commutative_plus (succ n) m)226 #n #m >(commutative_plus_pos (succ n) m) 227 227 <(plus_n_succm …) //; qed. 228 228 … … 775 775 ] qed. 776 776 777 theorem minus_n_n : ∀n:Pos.one=nn.777 theorem minus_n_n_pos: ∀n:Pos.one=nn. 778 778 #n normalize; >(partial_minus_n_n n) //; 779 779 qed. … … 877 877 qed. 878 878 879 theorem minus_to_plus :∀n,m,p:Pos.879 theorem minus_to_plus_pos :∀n,m,p:Pos. 880 880 m < n → nm = p → n = m+p. 881 881 #n #m #p #lemn #eqp applyS plus_minus_m_m; //; 882 882 qed. 883 883 884 theorem plus_to_minus :∀n,m,p:Pos.n = m+p → nm = p.884 theorem plus_to_minus_pos :∀n,m,p:Pos.n = m+p → nm = p. 885 885 (* /4/ done in 43.5 *) 886 886 #n #m #p #eqp
Note: See TracChangeset
for help on using the changeset viewer.