proposition: Lemma Rlt_0_inv_2 : 0 < / 2.
proof: Proof. assert (H : 1 < 2). pattern 1 at 1; rewrite <- (Rplus_0_r 1). apply Rplus_lt_compat_l; apply Rlt_0_1. apply Rmult_lt_reg_l with (r := 2). eapply Rlt_trans; [apply Rlt_0_1|apply H]. rewrite Rmult_0_r. replace (2 * / 2) with 1; [apply Rlt_0_1|]. rewrite Rmult_comm; symmetry; apply Rinv_l. intros Hneg. apply (Rlt_asym 1 0). rewrite <- Hneg; apply H. apply Rlt_0_1. Qed.
imports: Reals Lia Lra