proposition: Lemma ratMult_0_l : forall r, 0 * r == 0.
proof: Proof. intuition; destruct r. unfold ratMult. simpl. unfold natToPosnat, posnatMult; simpl. destruct p. apply rat_num_0. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms