proposition: Lemma total_meet_either x y : meet x y = x |_| meet x y = y.
proof: Proof. destruct (total le x y) as [E|E]. - left. apply meet_l,E. - right. apply meet_r,E. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.semirings HoTT.Classes.theory.lattices