proposition: Lemma Zeckp_prop3b n (e := Zeckp): Zeck_li n != 0 -> e (e n) = n - e n.
proof: Proof. rewrite /e - lt0n => /Zeck_li_prop2 => h. rewrite {2} (Zeckp_prop2 n) addKn; apply:(Zeckp_prop1_bis h (Zeck_uniq n)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)