proposition: Lemma meet_join_eq : forall x y : X, meet x y == join x y -> x == y.
proof: Proof. intros. rewrite <- (meet_join_absorb_l_l y x). rewrite -> (join_comm X y x). rewrite <- H. rewrite -> (meet_comm X x y). rewrite -> (meet_assoc X). rewrite -> (meet_idem X). set (RHS := meet y x). rewrite <- (meet_join_absorb_l_l x y). rewrite <- H. rewrite -> (meet_assoc X). rewrite -> (meet_idem X). rewrite -> (meet_comm X). reflexivity. Qed.
imports: Coq.Setoids.Setoid CoRN.order.SemiLattice