proposition: Lemma plus_correct : forall i1 i2 x1 x2, to_p i1 x1 -> to_p i2 x2 -> to_p (plus i1 i2) (x1+x2).
proof: Proof. intros i1 i2 x1 x2 H1 H2. destruct i1 as [[l1 | | ][u1 | | ]]; generalize H1; simpl; clear H1; intros H1; contradiction || auto; destruct i2 as [[l2 | | ][u2 | | ]]; generalize H2; simpl; intros; contradiction || auto; try lia. Qed.
imports: ZArith List Lia