proposition: Lemma vec_order_large_morph dim : forall x x' : vector dim, eq_vec x x' -> forall y y', eq_vec y y' -> (vec_order_large _ x y <-> vec_order_large _ x' y').
proof: Proof. induction dim. simpl. intros. rewrite H;rewrite H0;reflexivity. simpl. intros [a1 v1] [a1' v1'] [Heq1 Heq2] [a2 v2] [a2' v2'] [Heq3 Heq4]. rewrite Heq1;rewrite Heq3. destruct (IHdim _ _ Heq2 _ _ Heq4) as [IH1 IH2]. intuition. Defined.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)