proposition: Lemma Saleph_inv A M: Saleph A -> A \Eq M -> Saleph M.
proof: Proof. move =>[ha [r wor]] cam; split; first exact:(Sinfinite_inv ha cam). move: cam =>[f fp]; move: (worder_transportation wor fp) =>[s wos _]. by exists s. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)