proposition: Lemma product2_canon_fb x y: bijection (product2_canon x y).
proof: Proof. rewrite /product2_canon. move: (setX2_canon_axiom (x:=x) (y:=y)) => pa. apply: lf_bijective=>//. move => u v /setX_P [up pux quy] /setX_P [vp pvx qvy] eq. move :(congr1 (Vg ^~ C0) eq) (congr1 (Vg ^~ C1) eq); aw. by apply: pair_exten=>//. move=> z /setX2_P [fz dz Va Vb]. exists (J (Vg z C0) (Vg z C1)); aww. symmetry;apply: fgraph_exten;fprops; aw;try ue. by move=> t td; try_lvariant td. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)