proposition: Lemma Rgen_phiPOS : forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x > 0.
proof: Proof. unfold Rgt. induction x; simpl; intros. - apply Rlt_trans with (1 + 0). + rewrite Rplus_comm. apply Rlt_n_Sn. + apply Rplus_lt_compat_l. rewrite <- (Rmul_0_l Rset Rext RTheory 2). rewrite Rmult_comm. apply Rmult_lt_compat_l. * apply Rlt_0_2. * trivial. - rewrite <- (Rmul_0_l Rset Rext RTheory 2). rewrite Rmult_comm. apply Rmult_lt_compat_l. + apply Rlt_0_2. + trivial. - replace 1 with (0 + 1). + apply Rlt_n_Sn. + apply Rplus_0_l. Qed.
imports: Nnat ArithRing Ring Field Rdefinitions Rpow_def Raxioms