proposition: Lemma ch_nat_ch l v: match (ch_nat l v) with | Some k => nat_ch (Some k) l = Some v | _ => true end.
proof: Proof. induction l. - rewrite ch_nat_equation_1. simpl. rewrite nat_ch_aux_equation_1. by destruct v. - rewrite ch_nat_equation_2. simpl. rewrite nat_ch_aux_equation_9. reflexivity. - rewrite ch_nat_equation_3. simpl. rewrite nat_ch_aux_equation_10. destruct v ; reflexivity. - destruct v. rewrite ch_nat_equation_4. simpl. specialize (IHl1 s). specialize (IHl2 s0). move: IHl1 IHl2. case (ch_nat l1 s) ; case (ch_nat l2 s0). + simpl. intros. rewrite nat_ch_aux_equation_32. by rewrite IHl1 IHl2. + by simpl ; intros ; try inversion IHl1 ; try inversion IHl2. + by simpl ; intros ; try inversion IHl1 ; try inversion IHl2. + by simpl ; intros ; try inversion IHl1 ; try inversion IHl2. - rewrite ch_nat_equation_5. done. - destruct v eqn:e ; simpl. + rewrite ch_nat_equation_6. specialize (IHl s). case (ch_nat l s) eqn:e'. ++ simpl. intros. rewrite nat_ch_aux_equation_20. f_equal. done. ++ done. + rewrite ch_nat_equation_7. done. - rewrite ch_nat_equation_8. simpl. rewrite nat_ch_aux_equation_14. f_equal. unfold nat_ch_aux_obligation_1. have lv := ltn_ord v. apply /eqP. erewrite <- inj_eq. 2: apply ord_inj. simpl. rewrite modn_small. 2: assumption. done. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude RandomOracle) Coq(Utf8) extructures(ord fset fmap) Equations(Equations)