proposition: Lemma total_join_either `{!TotalRelation le} x y : join x y = x |_| join x y = y.
proof: Proof. destruct (total le x y) as [E|E]. - right. apply join_r,E. - left. apply join_l,E. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.semirings HoTT.Classes.theory.lattices