proposition: Lemma truncminus_0_r : ∏ x : X, truncminus ex x 0 = Lmax lat x 0.
proof: Proof. intros x. rewrite <- (runax _ (truncminus _ _ _)). apply (istruncminus_ex). Qed.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Algebra.Groups