proposition: Lemma Rlt_0_2 : 0 < 2.
proof: Proof. assert (H : 0 < 1) by exact Rlt_0_1. apply (Rlt_trans _ 1); try easy. replace 2 with (1 + 1) by reflexivity. rewrite <-(Rplus_0_l 1) at 1. apply Rplus_lt_le_compat; try easy. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField