proposition: Lemma fgraph_setU1 f x y: fgraph f -> ~ inc x (domain f) -> fgraph (f +s1 (J x y)).
proof: Proof. move => sa sb; move:(fgraph_set1 x y) => [ha hb hc]. apply:fgraph_setU2 => //; rewrite hb; apply: disjoint_pr => t td /set1_P tx. by case: sb; rewrite - tx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)