proposition: Lemma ratInverse_1 : ratInverse 1 == 1.
proof: Proof. unfold ratInverse. case_eq rat1; intuition. inversion H; clear H; subst. eapply eqRat_terms; trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms