proposition: Lemma miller_rabin_more_tests l l' : (forall x, In x l -> In x l') -> forall n, implb (miller_rabin l' n) (miller_rabin l n) = true.
proof: Proof. intros s n. unfold miller_rabin in *. destruct (_ <? _). reflexivity. destruct (_ =? _). reflexivity. destruct (Z.odd _). 2: reflexivity. destruct (remove_twos _). rewrite 2andb_true_l. assert (a : forall a b, (a = true -> b = true) -> implb a b = true) by now intros [|] [|]; try discriminate || tauto. apply a. rewrite 2forallb_forall. eauto. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)