proposition: Lemma det_range : #|{:image_type (@Tab_rc _ M)}| <= (#|M|.+1)^(#|M|.+1).
proof: Proof. pose table' := (option M * {ffun M -> option M})%type. apply: (@leq_trans #|{: table'}|); last by rewrite card_prod card_ffun !card_option expnS. pose f (x : image_type (@Tab_rc _ M)) : table' := let (b,_) := x in ([pick q | q \in b.1],[ffun p => [pick q | (p,q) \in b.2]]). suff : injective f by apply: leq_card. move => [[a1 a2] Ha] [[b1 b2] Hb] [E1 /ffunP E2]. apply: val_inj => /=. move: Ha Hb => /dec_eq /= [x Hx] /dec_eq [y Hy]. rewrite [Tab M x]surjective_pairing [Tab M y]surjective_pairing !xpair_eqE in Hx Hy. case/andP : Hx => /eqP ? /eqP ?. case/andP : Hy => /eqP ? /eqP ?. subst. f_equal. - apply/setP => p. case: (pickP _) E1 => q1; case: (pickP _) => q2 //; last by rewrite q1 q2. move => {E2} H1 H2 [?]; subst. wlog suff S : p x y H1 H2 / (p \in (Tab M x).1) -> (p \in (Tab M y).1). { apply/idP/idP; exact: S. } move => H. by rewrite (@Tab1_uniq x p q2). - apply/setP => [[p q]]. move: E2 {E1} => /(_ p). rewrite !ffunE. case: (pickP _) => r1; case: (pickP _) => r2 //; last by rewrite r1 r2. move => H1 H2 [?]; subst. apply/idP/idP => ?. + by rewrite (@Tab2_functional x p q r2). + by rewrite (@Tab2_functional y p q r2). Qed.
imports: Coq(Lia) mathcomp(all_ssreflect) RegLang(misc setoid_leq languages dfa myhill_nerode two_way)