proposition: Lemma choice_type_lt_tot : ∀ x y, (choice_type_lt x y || choice_type_lt y x || choice_type_eq x y).
proof: Proof. intros x y. destruct (choice_type_eq x y) eqn:H. - apply/orP. by right. - apply/orP. left. unfold choice_type_eq in H. pose (choice_type_lt_total_holds x y). move: i. move /implyP => i. apply i. apply/negP. intuition. move: H0. rewrite H. intuition. 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)