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