proposition: Fact interval_union_right i j x : in_interval j x -> in_interval (interval_union i j) x.
proof: Proof. revert i j; intros (a,b) (u,v); simpl. generalize (Nat.le_min_r a u) (Nat.le_max_r b v); lia. Qed.
imports: List Arith Nat Lia