proposition: Lemma cnvldv `{laws} `{CNV+DIV ≪ l} n m p (x: X n m) (y: X n p): (x -o y)° ≡ y° o- x°.
proof: Proof. apply from_below. intro z. cnv_switch. rewrite ldv_spec. cnv_switch. rewrite cnvdot, cnv_invol. now rewrite rdv_spec. Qed.
imports: lattice