proposition: Theorem asPreO : PreO.t MeetLat.le.
proof: Proof. constructor; simpl; intros. - apply dot_idempotent. - rewrite <- H. rewrite <- H0 at 2. rewrite dot_assoc. reflexivity. Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat