proposition: Lemma cnvneg `{laws} `{CNV+BL ≪ l} n m (x: X n m): (neg x)° ≡ neg (x°).
proof: Proof. apply neg_unique. rewrite <-cnvpls, cupC, cupneg. now rewrite cnvtop. rewrite <-cnvcap, capC, capneg. now rewrite cnv0. Qed.
imports: lattice