proposition: Lemma order_product2_P f g x x': gle (order_product2 f g) x x' <-> [/\ inc x ((substrate f) \times (substrate g)), inc x' ((substrate f)\times (substrate g)) & gle f (P x) (P x') /\ gle g (Q x) (Q x')].
proof: Proof. split; first by move/Zo_P =>[] /setXp_P; aw; move => [pa pb] pc. by move => [pa pb pc]; apply: Zo_i; [apply:setXp_i | aw ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)