proposition: Lemma matrix_3_ind : forall (P:(matrix 3) -> Type), forall (H:forall x_0_0 x_0_1 x_0_2 x_0_3, forall x_1_0 x_1_1 x_1_2 x_1_3 , forall x_2_0 x_2_1 x_2_2 x_2_3, forall x_3_0 x_3_1 x_3_2 x_3_3, P (x_0_0, ((x_0_1,(x_0_2,x_0_3)), ((x_1_0,(x_2_0,x_3_0)), (x_1_1, ((x_1_2,x_1_3), ((x_2_1,x_3_1), (x_2_2, (x_2_3, (x_3_2,x_3_3)))))))))), forall (m:matrix 3), P m.
proof: Proof. intros . refine match m with | (_, ((_,(_,_)),((_,(_,_)),(_,((_,_),((_,_),(_,(_,(_,_))))))))) => _ end; apply H. Defined.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)