proposition: Lemma choice_type_lt_total_holds : ∀ x y, ~~ (choice_type_test x y) ==> (choice_type_lt x y || choice_type_lt y x).
proof: Proof. intros x y. induction x as [ | | | x1 ih1 x2 ih2| x1 ih1 x2 ih2| x ih| x] in y |- *. all: try solve [ destruct y ; auto with solve_subterm; reflexivity ]. - destruct y. all: try (intuition; reflexivity). cbn. specialize (ih1 y1). specialize (ih2 y2). apply/implyP. move /nandP => H. apply/orP. destruct (choice_type_test x1 y1) eqn:Heq. + destruct H. 1: discriminate. move: ih2. move /implyP => ih2. specialize (ih2 H). move: ih2. move /orP => ih2. destruct ih2. * left. apply/orP. right. apply/andP. split. all: intuition auto. * right. apply/orP. right. apply/andP. intuition. move: Heq. move /eqP => Heq. rewrite Heq. apply/eqP. reflexivity. + destruct H. * move: ih1. move /implyP => ih1. specialize (ih1 H). move: ih1. move /orP => ih1. destruct ih1. -- left. apply/orP. left. assumption. -- right. apply/orP. left. assumption. * move: ih2. move /implyP => ih2. specialize (ih2 H). move: ih2. move /orP => ih2. destruct ih2. --- simpl in ih1. move: ih1. move /orP => ih1. destruct ih1. +++ left. apply/orP. left. assumption. +++ right. apply/orP. left. assumption. --- simpl in ih1. move: ih1. move /orP => ih1. destruct ih1. +++ left. apply/orP. left. assumption. +++ right. apply/orP. left. assumption. - destruct y. all: try (intuition; reflexivity). cbn. specialize (ih1 y1). specialize (ih2 y2). apply/implyP. move /nandP => H. apply/orP. destruct (choice_type_test x1 y1) eqn:Heq. + destruct H. 1: discriminate. move: ih2. move /implyP => ih2. specialize (ih2 H). move: ih2. move /orP => ih2. destruct ih2. * left. apply/orP. right. apply/andP. split. all: intuition auto. * right. apply/orP. right. apply/andP. intuition. move: Heq. move /eqP => Heq. rewrite Heq. apply/eqP. reflexivity. + destruct H. * move: ih1. move /implyP => ih1. specialize (ih1 H). move: ih1. move /orP => ih1. destruct ih1. -- left. apply/orP. left. assumption. -- right. apply/orP. left. assumption. * move: ih2. move /implyP => ih2. specialize (ih2 H). move: ih2. move /orP => ih2. destruct ih2. --- simpl in ih1. move: ih1. move /orP => ih1. destruct ih1. +++ left. apply/orP. left. assumption. +++ right. apply/orP. left. assumption. --- simpl in ih1. move: ih1. move /orP => ih1. destruct ih1. +++ left. apply/orP. left. assumption. +++ right. apply/orP. left. assumption. - destruct y. all: try (intuition; reflexivity). unfold choice_type_lt. unfold choice_type_test. rewrite -neq_ltn. apply /implyP. auto. Qed.
imports: Coq(Utf8 Lia) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples GenericRulesSimple) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr realsum seq all_algebra fintype) Crypt(Prelude Axioms) extructures(ord fset fmap) Mon(SPropBase) Equations(Equations)