proposition: Lemma lower_laws {h k} {X} {H: laws h X} {le: k ≪ h}: laws k X.
proof: Proof. constructor; [ intros; apply lower_lattice_laws | .. ]; try solve [ apply H | intro; apply H; eauto using lower_trans ]. right. apply dotx1. right. apply dot_leq. intro H'. right. intros. apply weq_leq. apply (lower_trans _ _ _ H') in le. apply dotplsx. intro H'. right. right. intros. apply weq_leq. apply (lower_trans _ _ _ H') in le. apply dotxpls. intro H'. right. intros. apply weq_leq. apply (lower_trans _ _ _ H') in le. apply dot0x. intro H'. right. right. intros. apply weq_leq. apply (lower_trans _ _ _ H') in le. apply dotx0. intro H'. right. intros. apply (lower_trans _ _ _ H') in le. apply cnv_ext. intro H'. right. right. apply (lower_trans _ _ _ H') in le. apply str_ind_r. Qed.
imports: lattice