proposition: Lemma ratMult_2 : forall r, r + r == r * (2/1).
proof: Proof. rattac. inversion H; clear H; subst. arithNormalize. rewrite Nat.mul_0_r. rewrite Nat.add_0_r. f_equal. f_equal. rewrite <- Nat.mul_assoc. rewrite <- Nat.mul_assoc. rewrite Nat.mul_comm. simpl. trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms