proposition: Lemma simple_fct2 a b (f := singleton (J a b)): [/\ fgraph f, domain f = singleton a, range f = singleton b, Vg f a = b & f = Lg (singleton a) (fun _ => b)].
proof: Proof. move: (fgraph_set1 a b) => [ha hb hc]; rewrite hb hc. move:(pr2_V ha (set1_1 (J a b))); aw => bv. split => //; apply: fgraph_exten => //; aww; rewrite hb => x /set1_P ->. rewrite LgV //; apply: set1_1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)