proposition: Lemma maximal_continuation_total o (o_max: ∀ o', o ≼ o' → o' ≼ o): ∀ x y, eqA x y ∨ o.R x y ∨ o.R y x.
proof: Proof. enough (∀ x, o.S x) by (intros; eapply R_carrier_complete; [apply (o.good)|auto..]). intro. destruct (classic (o.S x)) as [|notinx]; trivial. apply (o_max (suspend o x notinx)); [|now right]. split; cbn; auto. - now left. - intros y z [iny|eqy] inz [rel|[iny' eqz]]; eauto. destruct (o.good) as [_ _ _ _ correct _]. apply correct in rel. rewrite eqy in notinx; tauto. - intros y z iny inz. unfold suspend_R. split; [tauto|]. intros [|[_ eqxz]]; auto. clear -notinx inz eqxz. destruct o as [[S R] []]; cbn in *. now rewrite eqxz in notinx. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)