proposition: Lemma Sierpinski_step (X : HSet) n : GCH -> infinite X -> powfix X -> InjectsInto (HN X) (power_iterated X n) -> InjectsInto X (HN X).
proof: Proof. intros gch H1 H2 Hi. induction n. - now apply HN_ninject in Hi. - destruct (gch (Build_HSet (power_iterated X n)) (Build_HSet (power_iterated X n + HN X))) as [H|H]. + now apply infinite_power_iterated. + apply tr. exists inl. intros x x'. apply path_sum_inl. + eapply InjectsInto_trans. * apply InjectsInto_sum; try apply Hi. apply tr, Injection_power. exact _. * cbn. specialize (H2 (S n)). cbn in H2. rewrite H2. apply tr, Injection_refl. + apply IHn. eapply InjectsInto_trans; try apply H. apply tr. exists inr. intros x y. apply path_sum_inr. + apply InjectsInto_trans with (power_iterated X (S n)); try apply tr, Injection_power_iterated. cbn. apply (Cantor_injects_injects H). rewrite (H2 n). apply tr, Injection_refl. Qed.
imports: HoTT(TruncType ExcludedMiddle abstract_algebra) HoTT(PropResizing.PropResizing) HoTT(Spaces.Nat.Core Spaces.Card) HoTT(Equiv.BiInv) HoTT(HIT.unique_choice) HoTT.Sets(Ordinals Hartogs Powers GCH AC)