proposition: Lemma choice_type_lt_asymmetric : ∀ x y, (choice_type_lt x y ==> ~~ choice_type_lt y x).
proof: Proof. intros x y. apply /implyP. move => H. destruct (~~ choice_type_lt y x) eqn:Heq. - intuition. - move: Heq. move /negP /negP => Heq. pose (choice_type_lt_areflexive x) as Harefl. move: Harefl. apply /implyP. rewrite implyNb. apply /orP. left. apply (choice_type_lt_transitive _ _ _ H Heq). 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)