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