proposition: Lemma mat_order_large_trans dim : forall v1 v2 v3, mat_order_large dim v1 v2 -> mat_order_large _ v2 v3 -> mat_order_large _ v1 v3.
proof: Proof. induction dim. simpl. intros. apply o.(le_trans) with v2; assumption. simpl;intros [a1 [l1 [c1 m1]]] [a2 [l2 [c2 m2]]] [a3 [l3 [c3 m3]]] [H1 [H2 [H3 H4]]] [H5 [H6 [H7 H8]]];repeat split. apply o.(le_trans) with a2;assumption. apply (o_vec dim).(le_trans) with l2;assumption. apply (o_vec dim).(le_trans) with c2;assumption. apply IHdim with m2;assumption. Defined.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)