proposition: Lemma ratInverse_eqRat_compat : forall r1 r2, ~ r1 == 0 -> r1 == r2 -> ratInverse r1 == ratInverse r2.
proof: Proof. intuition. unfold ratInverse. destruct r1. destruct r2. destruct n. exfalso. eapply H. eapply rat_num_0. destruct n0. exfalso. eapply rat_num_nz. 2:{ rewrite rat_num_0 in H0. eauto. } lia. eapply eqRat_flip. eapply H0. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms