proposition: Lemma crt_double r : r ＊ ≡ r ^? ⨾ (r ⨾ r) ＊.
proof: Proof. split; [|by eauto 7 using inclusion_seq_trans, inclusion_rt_rt2 with hahn]. apply inclusion_rt_ind_left; eauto with hahn. rewrite !crE; autorewrite with hahn hahn_full. rewrite <- seqA, <- ct_begin; eauto with hahn. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets