proposition: Lemma if_not_prefix (H : kraft_cond R T l) : ~ prefix_code C -> [exists j : 'I_n, [exists k : 'I_n, (j < k) && prefix (sigma j) (sigma k)]].
proof: Proof. move/prefix_codeP => notprefix; move: (w_ub H) => w_ub. rewrite -(negbK ([exists j, _])) negb_exists. apply/negP => /forallP /= H'. apply notprefix => c c'. move/mapP => [/= a _ ->{c}] /mapP[/= b _ ->{c'}] ab size_ab. apply/negP => prefix_ab. move: (H' a). rewrite negb_exists => /forallP/(_ b); rewrite prefix_ab andbT -leqNgt => ba. move: size_ab; rewrite leqNgt => /negP; apply. rewrite ltn_neqAle; apply/andP; split. by rewrite eq_sym ltn_eqF // prefixW. rewrite size_sigma //; last by rewrite -/t -(card_ord t) w_sub. rewrite size_sigma //; last by rewrite -/t -(card_ord t) w_sub. move: ba; rewrite leq_eqVlt => /orP[/eqP ->//|ba]. by apply/(sorted_ltn_nth leq_trans) => //; rewrite inE l_n. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext