proposition: Lemma total_join_max x y : join x y = max x y.
proof: Proof. unfold max;destruct (total le x y) as [E|E]. - apply join_r,E. - apply join_l,E. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.semirings HoTT.Classes.theory.lattices