proposition: Lemma ratMult_1_l : forall r, 1 * r == r.
proof: Proof. rattac. inversion H; clear H; subst. repeat rewrite Nat.mul_1_l in *. trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms