proposition: Lemma iff_intro_Prop (P Q P' Q' : Prop) : (P <-> Q) -> (P -> Q -> (P' <-> Q')) -> ((P -> P') <-> (Q -> Q')).
proof: Proof. firstorder. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz List Bool) Coqtail(Ztools Zeqm Zlittle_fermat Zpow Zprime)