proposition: Lemma projected_bounded_sl: IsBoundedSemiLattice B.
proof: Proof. split. - apply (projected_com_monoid f);trivial. - repeat intro; apply (injective f). rewrite op_correct, (idempotency (+) _). trivial. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.groups