proposition: Lemma mult_resp_Npos0 : forall x y : nat, x <> 0 -> y <> 0 -> (x*y) <> 0.
proof: Proof. intros x y H H0. destruct (Npos_is_suc y H0) as [y0 H2]. rewrite H2 in H0. rewrite H2. generalize y0. clear H0 H2 y0 y. intro y0. induction y0 as [| y0 Hrecy0]. rewrite Nat.mul_comm. rewrite Nat.mul_1_l. exact H. rewrite <- mult_n_Sm. cut (0 <> (x*S y0+x) -> (x*S y0+x) <> 0). intro H3. apply H3. apply Nat.neq_sym. apply Nat.neq_0_lt_0. cut ((x*S y0+x) > 0). unfold gt in |- *. intuition. apply Nat.lt_trans with (x*S y0). apply Nat.lt_le_trans with (x*S y0+0). lia. lia. lia. lia. Qed.
imports: CoRN.model.structures.Nsec Coq(Arith Lia)