proposition: Fact mult_is_one p q : p*q = 1 -> p = 1 /\ q = 1.
proof: Proof. destruct p as [ | [ | p ] ]. + simpl; discriminate. + simpl; lia. + rewrite Nat.mul_comm. destruct q as [ | [ | q ] ]. - simpl; discriminate. - simpl; lia. - simpl; discriminate. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)