proposition: Lemma expansion_ext_aug_dim f n: inc f (expansions_ext_of n) -> n <> \0c -> expansion_ext_aug (expansion_ext_dim f) (Vg f \0c) = f.
proof: Proof. move => /Zo_hi [[[ n3 kN lt13[fgf df fp]] nv] kp] nz. case: (equal_or_not (cardinal (domain f)) \0c) => knz. case: nz; rewrite - nv; apply:csum_trivial; aw. by apply: card_nonempty. have [sa sb]:= (cpred_pr kN knz). rewrite /expansion_ext_dim /expansion_ext_aug. rewrite Lgd (card_nat sa) - sb. apply:fgraph_exten; [fprops | done | by aw | aw => x xi]. rewrite (LgV xi); Ytac xz; first by ue. move: (cpred_pr (NS_inc_nat kN xi) xz) => [sa' sb']; rewrite LgV//; first ue. apply/(NltP sa); apply/(cleSltP sa'); rewrite - sb'. by apply/(cltSleP sa); rewrite - sb; apply /(NltP kN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)