proposition: Theorem series_left_shift_0 : ∀ s, (series_left_shift 0 s = s)%ser.
proof: Proof. intros s. unfold series_left_shift. destruct s; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Puiseux_series Ps_add Ps_add_compat Ps_mul Power_series