proposition: Lemma restr_exten x f g: {inc x, f =1g g} -> restr f x = restr g x.
proof: Proof. move => Ha; apply:fgraph_exten; try apply: restr_fgraph; rewrite !restr_d //. by move => t tx /=; rewrite !restr_ev // Ha. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)