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

 1 edited
Legend:
 Unmodified
 Added
 Removed

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.