forall a b c : Q, meet (a + b) (a + c) = a + meet b c. Proof. intros. destruct (total le b c) as [E|E]. - rewrite (meet_l _ _ E). apply meet_l. apply (order_preserving (a +)),E. - rewrite (meet_r _ _ E). apply meet_r. apply (order_preserving (a +)),E. Qed.
Require Import Import Quoting.Instances. Import NatPair.Instances.