proposition: Lemma eq_vec_trans : forall dim (v1 v2 v3:vector dim), v1 ==v v2 -> v2 ==v v3 -> v1 ==v v3.
proof: Proof. exact (eq_vec_trans eq_Equivalence). Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)