proposition: Theorem asPO : PO.t MeetLat.le eql.
proof: Proof. constructor. - apply asPreO. - repeat intro; simpl; split; intros. rewrite <- H, <- H0. assumption. rewrite H, H0. assumption. - simpl. intros. rewrite <- H. rewrite <- H0 at 2. rewrite dot_comm. reflexivity. Qed.
imports: SetoidClass Coq.Classes.Morphisms Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat