proposition: Lemma truncminus_Lmin_l : ∏ k x y : X, truncminus ex (Lmin lat x y) k = Lmin lat (truncminus ex x k) (truncminus ex y k).
proof: Proof. intros k x y. eapply rcancel. { apply (is1 k). } simpl. rewrite is3, 2!istruncminus_ex. apply (pathscomp0 (istruncminus_ex _ _ _)). apply is4. Qed.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Groups