proposition: Lemma ratAdd_arg_0 : forall a b, a + b == a -> b == 0.
proof: Proof. intuition. eapply eqRat_ratAdd_same_r. rewrite ratAdd_comm. rewrite H. rewrite <- ratAdd_0_l. intuition. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms