proposition: Lemma matrix_1_ind : forall (P:(matrix 1) -> Type), forall (H:forall x_0_0 x_0_1, forall x_1_0 x_1_1, P (x_0_0, ((x_0_1,(x_1_0,x_1_1))))), forall (m:matrix 1), P m.
proof: Proof. intros . refine match m with | (_,(_,(_,_))) => _ end; vm_compute in *|- ; repeat (match goal with | H:_*_ |- _ => clear H end); apply H. Defined.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)