proposition: Lemma gs_decreasing : hd (tl s) ≤ hd s.
proof: Proof. destruct gs. apply (maps.order_reflecting_pos (.*.) r); try tauto. transitivity (hd (tl s)); try tauto. rewrite <- (rings.mult_1_l (hd (tl s))) at 2. apply semirings.mult_le_compat; try solve [apply orders.lt_le; tauto]. tauto. reflexivity. Qed.
imports: Limit abstract_algebra orders additional_operations streams series