proposition: Lemma all_mem_pos_def : forall l, (forall c, In c l -> 0<= c) <-> all_mem_pos l.
proof: Proof. intro l;split;intro H. induction l. simpl. trivial. simpl. split. apply H;simpl;auto. apply IHl;intro;simpl in H;auto. functional induction (all_mem_pos l). simpl;tauto. destruct H;simpl. intros x H';simpl in H';destruct H'. subst. assumption. auto. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)