proposition: Lemma Zplus_minus : forall n m, n + (m - n) = m.
proof: Proof. Proof (fun n m => eq_trans (Z.add_comm n (m-n)) (Z.sub_add n m)). Lemma Zminus_plus_simpl_l : forall n m p, p + n - (p + m) = n - m. Proof (fun n m p => Z.add_add_simpl_l_l p n m). Lemma Zminus_plus_simpl_l_reverse : forall n m p, n - m = p + n - (p + m). Proof (SYM3 Zminus_plus_simpl_l). Lemma Zminus_plus_simpl_r : forall n m p, n + p - (m + p) = n - m. Proof (fun n m p => Z.add_add_simpl_r_r n p m). Lemma Zeq_minus : forall n m, n = m -> n - m = 0. Proof (fun n m => proj2 (Z.sub_move_0_r n m)). Lemma Zminus_eq : forall n m, n - m = 0 -> n = m. Proof (fun n m => proj1 (Z.sub_move_0_r n m)). Lemma Zmult_0_r_reverse : forall n, 0 = n * 0. Proof (SYM1 Z.mul_0_r). Lemma Zmult_assoc_reverse : forall n m p, n * m * p = n * (m * p). Proof (SYM3 Z.mul_assoc). Lemma Zmult_integral : forall n m, n * m = 0 -> n = 0 \/ m = 0. Proof (fun n m => proj1 (Z.mul_eq_0 n m)). Lemma Zmult_integral_l : forall n m, n <> 0 -> m * n = 0 -> m = 0. Proof (fun n m H H' => Z.mul_eq_0_l m n H' H). Lemma Zopp_mult_distr_l : forall n m, - (n * m) = - n * m. Proof (SYM2 Z.mul_opp_l). Lemma Zopp_mult_distr_r : forall n m, - (n * m) = n * - m. Proof (SYM2 Z.mul_opp_r). Lemma Zmult_minus_distr_l : forall n m p, p * (n - m) = p * n - p * m. Proof (fun n m p => Z.mul_sub_distr_l p n m). Lemma Zmult_succ_r_reverse : forall n m, n * m + n = n * Z.succ m. Proof (SYM2 Z.mul_succ_r). Lemma Zmult_succ_l_reverse : forall n m, n * m + m = Z.succ n * m. Proof (SYM2 Z.mul_succ_l). Lemma Zpos_eq : forall p q, p = q -> Z.pos p = Z.pos q. Proof. congruence. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass