proposition: Lemma choice_type_leqP : Ord.axioms choice_type_leq.
proof: Proof. split => //. - intro x. unfold choice_type_leq. apply/orP. left. apply /eqP. reflexivity. - intros v u w h1 h2. move: h1 h2. unfold choice_type_leq. move /orP => h1. move /orP => h2. destruct h1. + move: H. move /eqP => H. destruct H. apply/orP. assumption. + destruct h2. * move: H0. move /eqP => H0. destruct H0. apply/orP. right. assumption. * apply/orP. right. exact (choice_type_lt_transitive _ _ _ H H0). - unfold antisymmetric. move => x y. unfold choice_type_leq. move/andP => [h1 h2]. move: h1 h2. unfold choice_type_leq. move /orP => h1. move /orP => h2. destruct h1. 1:{ move: H. move /eqP. intuition auto. } destruct h2. 1:{ move: H0. move /eqP. intuition auto. } destruct (~~ (choice_type_test x y)) eqn:Heq. + move: Heq. move /idP => Heq. pose (choice_type_lt_total_not_holds x y) as Hp. move: Hp. move /implyP => Hp. specialize (Hp Heq). move: Hp. move /nandP => Hp. destruct Hp. * move: H. move /eqP /eqP => H. rewrite H in H1. simpl in H1. discriminate. * move: H0. move /eqP /eqP => H0. rewrite H0 in H1. simpl in H1. discriminate. + move: Heq. move /eqP. auto. - unfold total. intros x y. unfold choice_type_leq. pose (choice_type_lt_tot x y). move: i. move /orP => H. destruct H. + move: H. move /orP => H. destruct H. * apply/orP. left. apply/orP. right. assumption. * apply/orP. right. apply/orP. right. assumption. + apply/orP. left. apply/orP. left. 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)