proposition: Lemma OpenUnit_Dual_lt_1 : forall (a:OpenUnit), 1-a < 1.
proof: Proof. intros [a [H0 H1]]. simpl. rewrite -> Qlt_minus_iff. replace RHS with a by simpl; ring. assumption. Qed.
imports: Coq.QArith.QArith CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields CoRN.tactics.Qauto CoRN.tactics.CornTac