proposition: Lemma mult_strext0 : forall x1 x2 y1 y2 : nat, (x1*y1{#N}x2*y2) -> (x1{#N}x2) or (y1{#N}y2).
proof: Proof. unfold ap_nat in |- *. intros x1 x2 y1 y2 H. cut ({x1 = x2} + {x1 <> x2}). intro H1. elim H1. intro e. right. red in |- *. intro H0. apply H. exact (f_equal2 mult e H0). intro X. auto. apply eq_nat_dec. Qed.
imports: Coq.Arith.Peano_dec Coq.Relations.Relations CoRN.logic.CLogic Coq(Lia)