proposition: Lemma le_matrix_1_ind : forall (P:forall (m1 m2:matrix 1), (mat_order_large _ m1 m2) ->Prop), forall (H: forall x_0_0 x_0_1, forall x_1_0 x_1_1, forall y_0_0 y_0_1, forall y_1_0 y_1_1, forall (H_0_0:le x_0_0 y_0_0), forall (H_0_1:le x_0_1 y_0_1), forall (H_1_0:le x_1_0 y_1_0), forall (H_1_1:le x_1_1 y_1_1), P (x_0_0, (x_0_1, (x_1_0,x_1_1))) (y_0_0, (y_0_1, (y_1_0, y_1_1))) (conj H_0_0 (conj H_0_1 (conj H_1_0 H_1_1))) ), forall (m1 m2:matrix 1), forall (H:mat_order_large _ m1 m2), P m1 m2 H.
proof: Proof. intros . induction m1 using matrix_1_ind. induction m2 using matrix_1_ind. simpl in H0|-. refine match H0 with | (conj _ (conj _ (conj _ _))) => _ end. apply H. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)