proposition: Lemma Qlt_strext_unfolded : forall x1 x2 y1 y2 : Q, (x1<y1) -> (x2<y2) or (x1/=x2) or (y1/=y2).
proof: Proof. Proof with auto. intros x1 x2 y1 y2 E. destruct (Q_dec x2 y2) as [[|] | ]... destruct (Qeq_dec x1 x2) as [G | ]... right. right. apply Qnot_eq_sym, Qlt_not_eq. apply Qlt_trans with x2... eapply Qlt_compat. symmetry. apply G. reflexivity. assumption. right. destruct (Qeq_dec x1 y2) as [G|G]. right. apply Qnot_eq_sym, Qlt_not_eq. eapply Qlt_compat. symmetry. apply G. reflexivity. assumption. left. unfold Qap. intro F. apply G. transitivity x2... Qed.
imports: CoRN.logic.CLogic Coq.Arith.Arith Coq.Arith.Peano_dec CoRN.model.structures.Zsec Coq.QArith.QArith CoRN.stdlib_omissions.Q