proposition: Lemma extension_f_injective x f g a b: function f -> function g -> target f = target g -> source f = source g -> ~ (inc x (source f)) -> (extension f x a = extension g x b) -> f = g.
proof: Proof. move=> ff fg teq seq nixsf sv. rewrite - (extension_restr a ff nixsf) sv seq teq extension_restr //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)