proposition: Fact divides_lt p q : q < p -> divides p q -> q = 0.
proof: Proof. intros H1 ([ | k] & H2); auto. revert H2; simpl; generalize (k *p); intros; lia. Qed.
imports: Arith Lia List Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd sums rel_iter bool_nat power_decomp prime)