proposition: Lemma pidl_gleP1 i j k l: gle (prod_of_relation r1 r2) (J i j) (J k l) <-> gle r1 i k /\ gle r2 j l.
proof: Proof. split; first by move/pidl_gleP => [_ _ ] ; aw. move => [ha hb]; apply/pidl_gleP; split; aww. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)