proposition: Lemma mat_order_large_morph dim : forall x x' : matrix dim, eq_mat x x' -> forall y y', eq_mat y y' -> (mat_order_large _ x y <-> mat_order_large _ x' y').
proof: Proof. induction dim. simpl. intros. rewrite H;rewrite H0;reflexivity. simpl. intros [a1 [l1 [c1 m1]]] [a1' [l1' [c1' m1']]] [Heq1 [Heq2 [Heq3 Heq4]]] [a2 [l2 [c2 m2]]] [a2' [l2' [c2' m2']]] [Heq5 [Heq6 [Heq7 Heq8]]]. rewrite Heq1;rewrite Heq5. destruct (IHdim _ _ Heq4 _ _ Heq8) as [IH1 IH2]. rewrite Heq2; rewrite Heq3; rewrite Heq7; rewrite Heq6. intuition. Defined.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)