proposition: Fact own_multiple x p : x = p*x -> x = 0 \/ p = 1.
proof: Proof. destruct x as [ | x ]. + left; trivial. + right. destruct p as [ | [ | p ] ]. - simpl in H; discriminate. - trivial. - exfalso; revert H. do 2 (rewrite Nat.mul_comm; simpl). generalize (p*x); intros; lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)