proposition: Lemma tail_length : forall A (l1 l2:list A), length l1 = length l2 -> length (tail l1) = length (tail l2).
proof: Proof. induction l1 as [|x l1];destruct l2 as [|y l2];intros Hlength;simpl in Hlength; try discriminate Hlength;simpl;auto. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)