proposition: Lemma dual_laws l X (L: laws l X): laws l X^op.
proof: Proof. constructor; simpl; repeat right; intros. apply lattice_laws. symmetry. apply dotA. apply dotx1. apply dot1x. now apply dot_leq. apply weq_leq, dotxpls. apply weq_leq, dotplsx. apply weq_leq, dotx0. apply weq_leq, dot0x. apply weq_leq, cnvdot. apply cnv_invol. now apply cnv_leq. rewrite dotA. apply cnv_ext. apply str_refl. apply str_snoc. now apply str_ind_r. now apply str_ind_l. apply itr_str_r. apply capxdot. apply rdv_spec. apply ldv_spec. Qed.
imports: lattice