proposition: Lemma ext_to_prod_rel_f r r': equivalence r -> equivalence r' -> function (ext_to_prod(canon_proj r)(canon_proj r')).
proof: Proof. move=> er er'; apply: ext_to_prod_f; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)