proposition: Lemma pow_bounded_n_total A s (r : relation A) n (TOT: n_total s r n) (DOMA: doma r s) (IRR: irreflexive (⋃i <= 2 * n, r ^^ (S i))) : r ^^ (S (2 * n)) ⊆ (⋃i < 2 * n, r ^^ (S i)).
proof: Proof. intros a b R; apply powE in R; desf. assert (I: forall i j (L: i < j < S (2 * n)), r ^+ (f i) (f j)). { clear - R1; intros; desc. revert L0. rewrite (le_plus_minus _ _ L); generalize (j - S i) as k. revert R1; generalize (2 * n + 1) as m; ins. induction k; rewrite ?Nat.add_0_r; vauto. apply t_step, R1; lia. eapply t_trans, t_step; [apply IHk; lia|]. rewrite Nat.add_succ_r; apply R1; lia. } tertium_non_datur (exists i j, i < j <= n /\ f (2 * i) = f (2 * j)) as [C|C]; desc. { exists (2 * i + (2 * n - 2 * j)); split; try lia. rewrite <- Nat.add_succ_r. hahn_rewrite pow_add; exists (f (2 * i)); splits. apply powE; exists f; splits; ins; eapply R1; lia. rewrite C0; apply powE; exists (fun n => f (2 * j + n)). splits; try (f_equal; lia). intros; rewrite Nat.add_succ_r; apply R1; lia. } forward eapply (TOT (map (fun x => f (2 * x)) (List.seq 0 (S n)))). by rewrite length_map, length_seq; ins. { apply nodup_map; auto using nodup_seq; red; intros. rewrite in_seq0_iff in *. destruct (lt_eq_lt_dec x y) as [[L|]|L]; desf; eapply C. eexists x, y; splits; ins; lia. eexists y, x; splits; ins; lia. } all: intros; desf; rewrite in_map_iff in *; desc; rewrite in_seq0_iff in *; desf. eapply DOMA, R1; lia. assert (K: r ^^ (S (2 * x0 + (2 * n + 1 - 2 * x))) (f 0) (f (S (2 * n)))). { assert (K: r ^^ (2 * x0) (f 0) (f (2 * x0))). apply powE; exists f; splits; ins; eapply R1; lia. assert (L: r ^^ (2 * n + 1 - 2 * x) (f (2 * x)) (f (S (2 * n)))). { apply powE; exists (fun n => f (2 * x + n)); rewrite ?Nat.add_0_r. rewrite le_plus_minus_r; splits; intros; try done; try lia. f_equal; lia. rewrite Nat.add_succ_r; apply R1; lia. } rewrite <- Nat.add_succ_l, <- Nat.add_1_r. do 2 hahn_rewrite pow_add; unfold seq; repeat eexists; eauto. } destruct (lt_eq_lt_dec x0 x) as [[]|]; desf. - eexists; split; try exact K; lia. - edestruct IRR. exists (2 * x0 - 2 * x); split; try lia. eexists; split; [apply powE|edone]. exists (fun n => f (n + 2 * x)); splits; intros; try (f_equal; lia); apply R1; lia. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom