proposition: Lemma le_double : forall m n:nat, (2 * m <= 2 * n)%nat -> (m <= n)%nat.
proof: Proof. intros; apply INR_le. assert (H1 := le_INR _ _ H). do 2 rewrite mult_INR in H1. apply Rmult_le_reg_l with (INR 2). - apply lt_0_INR. apply Nat.lt_0_2. - assumption. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun ArithRing