proposition: Lemma vec_order_large_trans dim : forall v1 v2 v3, vec_order_large dim v1 v2 -> vec_order_large _ v2 v3 -> vec_order_large _ v1 v3.
proof: Proof. induction dim. simpl. intros. apply o.(le_trans) with v2; assumption. simpl;intros [a1 v1] [a2 v2] [a3 v3] [H1 H2] [H3 H4];split. apply o.(le_trans) with a2;assumption. apply IHdim with v2;assumption. Defined.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)