proposition: Lemma plus_strext0 : forall x1 x2 y1 y2 : nat, (x1+y1{#N}x2+y2) -> (x1{#N}x2) or (y1{#N}y2).
proof: Proof. intros x1 x2 y1 y2 H. unfold ap_nat in |- *. unfold ap_nat in H. case (eq_nat_dec x1 x2). intro e. right. red in |- *. intro H0. apply H. auto. intro n. left. intro H0. elim n. assumption. Qed.
imports: Coq.Arith.Peano_dec Coq.Relations.Relations CoRN.logic.CLogic Coq(Lia)