proposition: Lemma expansion_ext_dim_aug f n i: inc f (expansions_ext_of n) -> expansion_ext_dim (expansion_ext_aug f i) = f.
proof: Proof. move => /Zo_hi [[[ n3 kN lt13[fgf df fp]] nv] kp]. rewrite /expansion_ext_dim /expansion_ext_aug. rewrite Lgd (card_nat (NS_succ kN)) (cpred_pr2 kN). apply:fgraph_exten; [fprops | done | by aw | aw => x xi]. have ha := (NS_inc_nat kN xi). rewrite !LgV//. by rewrite (Y_false (@succ_nz x)) (cpred_pr2 ha). by apply /(NleP kN) /(cleSltP ha) /(NltP kN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)