proposition: Lemma matrix_2_ind : forall (P:(matrix 2) -> Type), forall (H:forall x_0_0 x_0_1 x_0_2, forall x_1_0 x_1_1 x_1_2, forall x_2_0 x_2_1 x_2_2, P (x_0_0, ((x_0_1,x_0_2),((x_1_0,x_2_0), (x_1_1, (x_1_2, (x_2_1,x_2_2)))))) ), forall (m:matrix 2), 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)