proposition: Lemma choice_type_lt_areflexive : ∀ x, ~~ choice_type_lt x x.
proof: Proof. intros x. induction x as [ | | | x1 ih1 x2 ih2 | x1 ih1 x2 ih2 | x ih | x] in |- *. all: intuition; simpl. - simpl. apply/norP. split. + apply ih1. + apply/nandP. right. apply ih2. - simpl. apply/norP. split. + apply ih1. + apply/nandP. right. apply ih2. - rewrite ltnn. 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)