proposition: Lemma expansion_prop15 f g b n: expansion f b n -> expansion g b n -> ( (expansion_value f b) <c (expansion_value g b) <-> exists k, [/\ k <c n, (Vg f k) <c (Vg g k) & (forall i, k <c i -> i <c n -> Vg f i = Vg g i)]).
proof: Proof. move => ha hb; split. case/(expansion_prop14 ha hb); first by move => [l [sa /(cleNgt sa) sb _]]. move => [l [m [hc hd he [hf hi hj hk]]]]; exists l; split => //. apply:clt_leT he hc. move => i la lb; case: (cleT_el (proj31 hc) (proj32_1 la)) => lc. rewrite hf // hi //. by apply: hj. move => [k [hc hd he]]. have nn := (cleR (proj32_1 hc)). by apply:(expansion_prop12 nn nn hc) he ha hb hd => i la /(cleNgt la). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)