proposition: Lemma ex3 n : (n + 4 %| 3 * n + 32) = (n \in [:: 0; 1; 6; 16]).
proof: Proof. apply/idP/idP => [Hn|]; rewrite !inE; last first. by move=> /or4P[] /eqP->. have : n + 4 %| 3 * n + 32 - 3 * (n + 4) by rewrite dvdn_sub// dvdn_mull. by rewrite mulnDr subnDl /= {Hn}; move: n; do 21?[case=>//]. Qed.
imports: mathcomp(all_ssreflect)