proposition: Lemma ratMult_same_r_inv : forall r1 r2 r3, r1 * r2 == r3 * r2 -> ~ r2 == 0 -> r1 == r3.
proof: Proof. intuition. unfold ratMult in *. destruct r1. destruct r2. destruct r3. unfold eqRat, beqRat in *. simpl in *. unfold posnatMult, posnatToNat, natToPosnat in *. destruct p1. destruct p0. destruct p. destruct (eq_nat_dec (n * n0 * (x * x0)) (n1 * n0 * (x1 * x0))); try congruence. destruct (eq_nat_dec (n * x) (n1 * x1)). trivial. exfalso. eapply n2. clear n2. arithNormalize. rewrite <- (Nat.mul_assoc n) in e. rewrite (Nat.mul_comm n0) in e. arithNormalize. rewrite <- Nat.mul_assoc in e. rewrite <- (Nat.mul_assoc n1) in e. rewrite <- (Nat.mul_comm x1) in e. rewrite (Nat.mul_assoc n1) in e. rewrite <- (Nat.mul_assoc (n1 * x1)) in e. eapply mult_same_r. 2:{ eapply e. } rewrite Nat.mul_0_r in H0. rewrite Nat.add_0_l in H0. destruct (eq_nat_dec n0 0). intuition. assert (~n0 * x0 = O)%nat. intros H1. eapply Nat.eq_mul_0 in H1. intuition. remember (n0 * x0)%nat as a. lia. lia. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms