proposition: Lemma get_elem_swap : forall m n (M : matrix m n) i j (ip : i < m) (jp : j < n), Vnth (get_row M ip) jp = Vnth (get_col M jp) ip.
proof: Proof. induction M; intros. lia. destruct i. trivial. simpl. rewrite IHM. trivial. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)