proposition: Lemma Rmult_ge_compat : forall r1 r2 r3 r4, r2 >= 0 -> r4 >= 0 -> r1 >= r2 -> r3 >= r4 -> r1 * r3 >= r2 * r4.
proof: Proof. intros r1 r2 r3 r4 H1%Rge_le H2%Rge_le I%Rge_le J%Rge_le; apply Rle_ge. now apply Rmult_le_compat. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField