proposition: Lemma equivalence_prod_of_rel r r': equivalence r -> equivalence r' -> equivalence (prod_of_relation r r').
proof: Proof. move => pa pb. apply: equivalence_from_rel; split. move => a b [ra rb];split; equiv_tac. move => a b c [ra rb] [rc rd];split; equiv_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)