proposition: Lemma Sprod_fgraph A B: fgraph A -> fgraph B -> fgraph (Sprod A B).
proof: Proof. move => [ha hb] [hc hd]; split. by move => x /Sprod_P [a [b [c [d [_ _ ->]]]]]; fprops. move => x y / Sprod_P[a [b [c [d [pa pb ->]]]]] /Sprod_P [a' [b' [c' [d' [pc pd ->]]]]]. aw => eq1; rewrite - eq1. move: (hb _ _ pa pc); aw => ea; rewrite - (pr2_def (ea (pr1_def eq1))). by move: (hd _ _ pb pd); aw => eb; rewrite - (pr2_def (eb (pr2_def eq1))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)