proposition: Theorem ratMult_0 : forall r1 r2, r1 * r2 == 0 <-> r1 == 0 \/ r2 == 0.
proof: Proof. intuition. rattac. rewrite Nat.mul_0_l in e. unfold posnatToNat in *. simpl in *. rewrite Nat.mul_1_r in e. apply Nat.eq_mul_0 in e. intuition; subst. left. apply rat_num_0. right. apply rat_num_0. rewrite <- (ratMult_0_l r2). eapply ratMult_eqRat_compat; intuition. rewrite <- (ratMult_0_r r1). eapply ratMult_eqRat_compat; intuition. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms