proposition: Theorem ratAdd_assoc : forall r1 r2 r3, r1 + r2 + r3 == r1 + (r2 + r3).
proof: Proof. rattac. inversion H; clear H; subst. Local Open Scope nat_scope. Ltac arithNormalize_step := repeat rewrite Nat.mul_succ_r in *; repeat rewrite Nat.mul_add_distr_r in *; repeat rewrite Nat.mul_add_distr_l in *; repeat rewrite Nat.mul_sub_distr_r in *; repeat rewrite Nat.mul_sub_distr_l in *; repeat rewrite Nat.add_assoc in *; repeat rewrite Nat.mul_assoc in *. Ltac arithNormalize := repeat arithNormalize_step. Ltac arithSimplify := match goal with | [|- _ + ?x = _ + ?x] => f_equal | [|- _ + (?x1 * ?x2) = _ + (?x2 * ?x1) ] => f_equal | [|- _ + (?x1 * ?x2 * ?x3) = _ + (?x1 * ?x3 * ?x2) ] => f_equal | [|- _ + (?x1 * ?x2 * ?x3 * ?x4 * ?x5 * ?x6) = _ + (?x1 * ?x3 * ?x2 * ?x4 * ?x5 * ?x6) ] => f_equal | [|- _ * ?x1 = _ * ?x1] => f_equal | [|- _ * ?x = _ ] => rewrite Nat.mul_comm; repeat rewrite Nat.mul_assoc; arithSimplify | [|- _ + ?x = _ ] => rewrite Nat.add_comm; repeat rewrite Nat.add_assoc; arithSimplify | [|- _ * ?x1 <= _ * ?x1] => apply Nat.mul_le_mono; auto | [|- _ * ?x1 <= _ * ?x1] => apply Nat.add_le_mono; auto | [|- _ * ?x <= _ ] => rewrite Nat.mul_comm; repeat rewrite Nat.mul_assoc; arithSimplify | [|- _ + ?x <= _ ] => rewrite Nat.add_comm; repeat rewrite Nat.add_assoc; arithSimplify end. arithNormalize. arithSimplify. arithSimplify. do 5 arithSimplify. do 5 arithSimplify. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms