fact: Definition prod_op {A B} (fA : A -> A -> Prop) (fB : B -> B -> Prop) (x y : A * B) := fA (fst x) (fst y) /\ fB (snd x) (snd y).
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat