proposition: Lemma set_seq_S_end_union_L `{!LeibnizEquiv C} start len : set_seq start (S len) =@{C} {[ start + len ]} ∪ set_seq start len.
proof: Proof. unfold_leibniz. apply set_seq_S_end_union. Qed.
imports: stdpp(finite) stdpp(options)