proposition: Lemma fgraph_set1 a b (f := singleton (J a b)): [/\ fgraph f, domain f = singleton a & range f = singleton b ].
proof: Proof. rewrite /f domain_set1 range_set1; split => //; split. move => i /set1_P ->; fprops. by move => i j /set1_P -> /set1_P ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)