proposition: Lemma matrix_rec : forall (P: forall dim, matrix dim -> Type) (f1: forall m, P 0 m) (f2: forall dim a r c m, P _ m -> P (S dim) (a,(r,(c,m)))) dim m, P dim m.
proof: Proof. intros P f1 f2 dim m. apply matrix_rect;assumption. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)