proposition: Lemma eqRat_ratMult_same_r : forall r1 r2 r3, ~r1 == 0 -> r2 * r1 == r3 * r1 -> r2 == r3.
proof: Proof. intuition. destruct r1. destruct r2. destruct r3. unfold ratMult in *. unfold eqRat in *. unfold beqRat in *. unfold ratCD in *. case_eq (0); intuition. rewrite H1 in H. destruct (eq_nat_dec (n * p2) (n2 * p)). intuition. destruct (eq_nat_dec (n0 * n * (posnatMult p1 p)) (n1 * n * (posnatMult p0 p))); intuition. inversion H1; clear H1; subst. unfold posnatMult, natToPosnat, posnatToNat in *. destruct p1. destruct p. destruct p0. destruct (eq_nat_dec (n0 * x) (n1 * x1)); trivial. exfalso. eapply n2. eapply (@mult_same_l (n * x0)). eapply mult_gt_0. rewrite Nat.mul_1_r in n3. rewrite Nat.mul_0_l in n3. lia. trivial. rewrite (Nat.mul_comm). rewrite Nat.mul_assoc. rewrite <- (Nat.mul_assoc n0). rewrite (Nat.mul_comm x). arithNormalize. rewrite e. do 3 arithSimplify. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms