proposition: Lemma choice_type_lt_total_not_holds : ∀ x y, ~~ (choice_type_test x y) ==> (~~ (choice_type_lt x y && choice_type_lt y x)).
proof: Proof. intros x y. apply /implyP. intros Hneq. pose (choice_type_lt_total_holds x y) as Htot. move: Htot. move /implyP => Htot. specialize (Htot Hneq). move: Htot. move /orP => Htot. apply /nandP. destruct Htot. - right. pose (choice_type_lt_asymmetric x y) as Hasym. move: Hasym. move /implyP => Hasym. specialize (Hasym H). assumption. - left. pose (choice_type_lt_asymmetric y x) as Hasym. move: Hasym. move /implyP => Hasym. specialize (Hasym H). assumption. 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)