proposition: Lemma isaprop_consecutive {X : Poset} (x y : X) : isaprop (consecutive x y).
proof: Proof. intros. unfold consecutive. apply isapropdirprod. - apply isapropdirprod. { apply pr2. } simpl. apply isapropneg. - apply impred; intro z. apply isapropneg. Defined.
imports: UniMath.Foundations.Propositions