proposition: Lemma Lg_fgraph p x: fgraph (Lg x p).
proof: Proof. split; first by move =>t /funI_P [z _ ->]; fprops. by move=> a b /funI_P [z1 _ ->] /funI_P [z2 _ ->]; aw => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)