proposition: Lemma all_mem_pos_tail : forall (l:list Z), all_mem_pos l -> all_mem_pos (tail l).
proof: Proof. intros l; functional induction all_mem_pos l. vm_compute;trivial. inversion 1;auto. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)