proposition: Lemma eq_vec_trans dim : forall (v1 v2 v3:vector dim), v1 ==v v2 -> v2 ==v v3 -> v1 ==v v3.
proof: Proof. induction v1 as [a|dim a1 v1] using vector_ind. simpl;intros v2 v3;intros;transitivity v2;assumption. simpl;intros [a2 v2] [a3 v3]. intuition. transitivity a2;assumption. apply IHv1 with v2;assumption. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)