proposition: Lemma nds_ax_perm X n f: natp n -> nds_ax X n -> inc f (permutations n) -> (nds_ax (fun z => X (Vf f z)) n /\ ordinalp (nds_sc X n f)).
proof: Proof. move=> nN ax => /Zo_P [ /functionsP [ff sf tf] bf]. have pc: nds_ax (fun z => X (Vf f z)) n. move => t /(NltP nN) tn; apply: ax; apply/(NltP nN); Wtac. by split => //; apply: OS_osumf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)