proposition: Lemma Rlt_0_2 : 0 < 2.
proof: Proof. apply Rlt_trans with (0 + 1). - apply Rlt_n_Sn. - rewrite Rplus_comm. apply Rplus_lt_compat_l. replace R1 with (0 + 1). + apply Rlt_n_Sn. + apply Rplus_0_l. Qed.
imports: Nnat ArithRing Ring Field Rdefinitions Rpow_def Raxioms