proposition: Lemma ap_Q_tight0 : forall x y : Q, Not (x/=y) <-> x==y.
proof: Proof. intros x y. red in |- *. split. unfold Qap in |- *. intro. case (Qeq_dec x y). intro e. assumption. intro n. elim H. intro H0. elim n. assumption. intro H. unfold Qap in |- *. red in |- *. intro H0. elim H0. assumption. Qed.
imports: CoRN.logic.CLogic Coq.Arith.Arith Coq.Arith.Peano_dec CoRN.model.structures.Zsec Coq.QArith.QArith CoRN.stdlib_omissions.Q