proposition: Lemma f_perm_t_ax f t: nat_ord_seq f -> inc t (permutations Nat) -> nat_ord_seq (f_perm_t f t).
proof: Proof. move => [ha hb hc] /permutationsP [/proj1/proj1 bt sf tt]. rewrite /f_perm_t; split; aw; fprops; hnf; aw => i iN; rewrite LgV//. apply:hc; rewrite hb; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)