proposition: Lemma pow_union_decomposition (n : nat) A (r r': relation A) : (r ∪ r')^^n ⊆ r'^^n ∪ (⋃k < n, r'^^k ⨾ r ⨾ (r ∪ r')^^(n - k - 1)).
proof: Proof. induction n using (well_founded_ind Wf_nat.lt_wf). destruct n as [| n']; [by firstorder|]. simpl (_ ^^ (S n')). rewrite !seq_pow_l, H; clear H; try done. autorewrite with hahn; autorewrite with hahn hahn_full. unionL; eauto with hahn. - unionR right; eapply inclusion_bunion_r with 0; ins; try lia; rels. replace (n' - 0) with n' by lia; eauto with hahn. - unionR right; eapply inclusion_bunion_r with 0; ins; try lia; rels. hahn_frame_l. arewrite (r ⊆ (r ∪ r') ^^ 1) at 1 by simpl; rels. arewrite (r' ⊆ r ∪ r') at 1; rewrite !pow_nm. replace (x + (1 + (n' - x - 1))) with (n' - 0) by lia; rels. - unionR right; eapply inclusion_bunion_r with (S x); ins; try lia; rels. by rewrite seq_pow_l, !seqA. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath