proposition: Lemma interval_trans x y z : x < y < z -> interval x y ++ interval y z = interval x z.
proof: Proof. revert z; funelim (interval x y); intros z H'; clear Heq. - simpl. destruct (lt_dec (S x) y); simpl. rewrite H; try lia. rewrite (interval_equation_1 x z). destruct lt_dec; simpl; trivial. elim n. lia. assert (y = S x) as -> by lia. rewrite interval_empty. simpl. rewrite (interval_equation_1 x z). destruct (lt_dec x z); trivial. elim n0; lia. - elim nltxy; lia. Qed.
imports: Equations(Equations) List Arith Lia