proposition: Lemma Is_true_neq_left x : x ≡ false → ¬Is_true x.
proof: Proof. intros E1 E2. pose proof (Is_true_eq_true x E2). subst. discriminate. Qed.
imports: CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax Coq.QArith.QArith Coq.Bool.Bool CoRN.metric2.Complete MathClasses.theory.CoqStreams MathClasses.interfaces.abstract_algebra MathClasses.theory.streams MathClasses.orders.naturals