proposition: Lemma ratSubtract_0_inv : forall r1 r2, ratSubtract r1 r2 == 0 -> r1 <= r2.
proof: Proof. intuition. unfold ratSubtract in *. rattac. rewrite Nat.mul_0_l in e. apply Nat.eq_mul_0 in e. lia. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms