proposition: Lemma IFS_suminjective: { inc (permutations Nat) &,injective sier_inf_sum}.
proof: Proof. move => s1 s2 hs1 hs2 sv. move: (IFE_osr s1) => [or1 sr1]. move: (IFE_osr s2) => [or2 sr2]. move: (order_type_exists or1). move: (order_type_exists or2). rewrite (OT_of_E hs2) (OT_of_E hs1) sv => is2 is1. move: (orderIT is1 (orderIS is2)) => [f isf] {sv is1 is2}. move/permutationsP:(hs1) =>[[[fs1 ijs1] [_ sjs1]] ss1 ts1]. move/permutationsP:(hs2) =>[[[fs2 ijs2] [_ sjs2]] ss2 ts2]. apply:function_exten => //; try ue. rewrite ss1 => n nN. have qa: cardinalp (Vf s1 n) by apply: CS_nat; rewrite /natp; Wtac. have qb: cardinalp (Vf s2 n) by apply: CS_nat; rewrite /natp; Wtac. apply (csucc_inj qa qb); clear qa qb. move:(isf) => [_ _ [bf sf tf] fm]. have ff: function f by fct_tac. case: (equal_or_not n \0c). move ->. move: (IFS_sub_pow_prop2 hs1 NS0) =>[x1 x1e1 cx10]. rewrite succ_zero in cx10. rewrite - (IFS_sub_pow_prop3 hs1 x1e1 cx10). rewrite - sr1 in x1e1. move: (sub_pow_pr0 isf x1e1). rewrite - sub_pow_pr1 - sub_pow_pr1 => eq2. have cc: cardinal (IFS_sub_pow s2 (Vf f x1)) = \1c. by rewrite - eq2 cx10. have x2s2: inc (Vf f x1) (IFSE s2) by rewrite - sr2 - tf; Wtac. by rewrite eq2 (IFS_sub_pow_prop3 hs2 x2s2 cc). move => nz; move: (cpred_pr nN nz)=> [pN pv]. rewrite pv; set p := cpred n; rewrite -/p in pN. move: (IFS_sub_pow_prop2 hs1 pN) =>[x1 x1e1 cx10]. move: (IFS_sub_pow_prop2 hs1 (NS_succ pN)) =>[x2 x2e1 cx20]. rewrite - (IFS_sub_pow_prop4 hs1 pN x1e1 x2e1 cx10 cx20). rewrite - sr1 in x1e1 x2e1. have y1s2: inc (Vf f x1) (IFSE s2) by rewrite - sr2 - tf; Wtac. have y2s2: inc (Vf f x2) (IFSE s2) by rewrite - sr2 - tf; Wtac. move: (sub_pow_pr0 isf x1e1) (sub_pow_pr0 isf x2e1). rewrite - ! sub_pow_pr1 => eqa eqb. have cc1: cardinal (IFS_sub_pow s2 (Vf f x1)) = (csucc p) by ue. have cc2: cardinal (IFS_sub_pow s2 (Vf f x2)) = (csucc (csucc p)) by ue. rewrite eqa eqb. by rewrite (IFS_sub_pow_prop4 hs2 pN y1s2 y2s2 cc1 cc2). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)