proposition: Lemma gs_positive : 0 ≤ hd s.
proof: Proof. destruct gs as [GS FA]. apply (maps.order_reflecting_pos (.*.) r); try tauto. rewrite rings.mult_0_r. transitivity (hd (tl s)); tauto. Qed.
imports: Limit abstract_algebra orders additional_operations streams series