proposition: Lemma ratSubtract_leRat_l: forall r1 r2 r3 : Rat, r1 <= r2 -> ratSubtract r1 r3 <= ratSubtract r2 r3.
proof: Proof. rattac. unfold ratSubtract in *. rattac. unfold posnatMult in *. inversion H4; clear H4; subst. inversion H3; clear H3; subst. arithNormalize. assert (n * x3 * x1 * x3 <= n0 * x3 * x2 * x3)%nat. apply Nat.mul_le_mono; trivial. rewrite <- (Nat.mul_comm x1). rewrite <- (Nat.mul_comm x2). repeat rewrite Nat.mul_assoc. apply Nat.mul_le_mono; trivial. rewrite Nat.mul_comm. rewrite l. rewrite Nat.mul_comm. trivial. assert (n3 * x2 * x1 * x3 = n3 * x1 * x2 * x3)%nat. do 3 arithSimplify. lia. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms