proposition: Lemma Zeckp_prop3a n (e := Zeckp): e (n + e n) = n.
proof: Proof. rewrite -{1 3}(Zeck_zeck_val n) /e {2}/Zeckp; move:(Zeckp_prop2_bis (Zeck n)). move => [Ha Hb Hc]; rewrite Hc - Ha. by apply:Zeckp_prop1; rewrite (map_inj_uniq succn_inj) Zeck_uniq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)