proposition: Lemma all_le_def : forall l1 l2, all_le l1 l2 <-> (length l1 = length l2 /\ forall x y, In (x,y) (combine l1 l2) -> x <= y).
proof: Proof. intros l1 l2;functional induction (all_le l1 l2). simpl;tauto. simpl. destruct l2. split;try tauto. split;try tauto. simpl;inversion 1;discriminate. simpl. split;try tauto. simpl;inversion 1;discriminate. simpl. destruct IHP as [lhs rhs]. split. intros [H1 H2]. destruct (lhs H2) as [Heq Hforall];split. f_equal. exact Heq. intros x' y' [h|h]. injection h;clear h;intros;subst;exact H1. auto. clear lhs. intros [H1 H2]. split;auto. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)