proposition: Lemma expe_p1 f k: expansion_ext f k -> inc f (sub_fgraphs Nat \3c).
proof: Proof. move => [ pa pb pc [pd pe pf]]. apply /sub_fgraphsP; exists k; first by apply:NS_inc_nat. apply/gfunctions_P2; split => // t /(range_gP pd) [x xdf ->]. by apply/(NltP NS3); apply: pf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)