forall a b c : Q, a < c -> b < c -> join a b < c. Proof. intros a b c E1 E2. destruct (total le a b) as [E3|E3];rewrite ?(join_r _ _ E3),?(join_l _ _ E3); trivial. Qed.
Require Import Import Quoting.Instances. Import NatPair.Instances.