proposition: Lemma pairhom_comp : pairhom [hom ga \o fa] [hom gb \o fb] = [hom pairhom ga gb \o pairhom fa fb].
proof: Proof. by apply /hom_ext/funext=> -[] x. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib category HB(structures)