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