proposition: Lemma Schroeder_l `{laws} `{BL+CNV ≪ l} n m p (x : X n m) (y : X m p) (z : X n p): x⋅y ≦ z <-> x°⋅!z ≦ !y.
proof: Proof. split. 2: apply Schroeder_. intro. apply Schroeder_. now rewrite 2negneg, cnv_invol. Qed.
imports: lattice