proposition: Lemma choice_type_lt_transitive : transitive (T:=choice_type) choice_type_lt.
proof: Proof. intros v u w h1 h2. induction u as [ | | | u1 ih1 u2 ih2 | u1 ih1 u2 ih2 | u ih | u] in v, w, h1, h2 |- *. - destruct w. all: try auto. destruct v. all: discriminate. - destruct w. all: try auto. all: destruct v. all: discriminate. - destruct w. all: try auto. all: destruct v. all: discriminate. - destruct v. all: try discriminate. all: destruct w. all: try discriminate. all: try reflexivity. cbn in *. move: h1 => /orP h1. move: h2 => /orP h2. apply/orP. destruct h1 as [h1|h1], h2 as [h2|h2]. + left. eapply ih1. all: eauto. + left. move: h2 => /andP [/eqP e h2]. subst. auto. + left. move: h1 => /andP [/eqP e h1]. subst. auto. + right. move: h1 => /andP [/eqP e1 h1]. move: h2 => /andP [/eqP e2 h2]. apply/andP. subst. split. * apply/eqP. reflexivity. * eapply ih2. all: eauto. - destruct v. all: try discriminate. all: destruct w. all: try discriminate. all: try reflexivity. simpl in *. move: h1 => /orP h1. move: h2 => /orP h2. apply/orP. destruct h1 as [h1|h1], h2 as [h2|h2]. + left. eapply ih1. all: eauto. + left. move: h2 => /andP [/eqP e h2]. subst. auto. + left. move: h1 => /andP [/eqP e h1]. subst. auto. + right. move: h1 => /andP [/eqP e1 h1]. move: h2 => /andP [/eqP e2 h2]. apply/andP. subst. split. * apply/eqP. reflexivity. * eapply ih2. all: eauto. - destruct v. all: try discriminate. all: destruct w. all: try reflexivity. all: try discriminate. simpl in *. eapply ih. all: eauto. - destruct v. all: try discriminate. destruct w. all: try discriminate. simpl in *. eapply ltn_trans. all: eauto. 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)