proposition: Lemma Zplus_assoc_reverse : forall n m p, n+m+p = n+(m+p).
proof: Proof. Proof (SYM3 Z.add_assoc). Lemma Zplus_succ_r_reverse : forall n m, Z.succ (n+m) = n+Z.succ m. Proof (SYM2 Z.add_succ_r). Notation Zplus_succ_r := Zplus_succ_r_reverse (only parsing). Lemma Zplus_0_r_reverse : forall n, n = n + 0. Proof (SYM1 Z.add_0_r). Lemma Zplus_eq_compat : forall n m p q, n=m -> p=q -> n+p=m+q. Proof (f_equal2 Z.add). Lemma Zsucc_pred : forall n, n = Z.succ (Z.pred n). Proof (SYM1 Z.succ_pred). Lemma Zpred_succ : forall n, n = Z.pred (Z.succ n). Proof (SYM1 Z.pred_succ). Lemma Zsucc_eq_compat : forall n m, n = m -> Z.succ n = Z.succ m. Proof (f_equal Z.succ). Lemma Zminus_0_l_reverse : forall n, n = n - 0. Proof (SYM1 Z.sub_0_r). Lemma Zminus_diag_reverse : forall n, 0 = n-n. Proof (SYM1 Z.sub_diag). Lemma Zminus_succ_l : forall n m, Z.succ (n - m) = Z.succ n - m. Proof (SYM2 Z.sub_succ_l). Lemma Zplus_minus_eq : forall n m p, n = m + p -> p = n - m. Proof. intros. now apply Z.add_move_l. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass