proposition: Lemma le_matrix_3_ind : forall (P:forall (m1 m2:matrix 3), (mat_order_large _ m1 m2) ->Prop), 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, forall y_0_0 y_0_1 y_0_2 y_0_3, forall y_1_0 y_1_1 y_1_2 y_1_3 , forall y_2_0 y_2_1 y_2_2 y_2_3, forall y_3_0 y_3_1 y_3_2 y_3_3, forall (H_0_0:le x_0_0 y_0_0), forall (H_0_1:le x_0_1 y_0_1), forall (H_0_2:le x_0_2 y_0_2), forall (H_0_3:le x_0_3 y_0_3), forall (H_1_0:le x_1_0 y_1_0), forall (H_1_1:le x_1_1 y_1_1), forall (H_1_2:le x_1_2 y_1_2), forall (H_1_3:le x_1_3 y_1_3), forall (H_2_0:le x_2_0 y_2_0), forall (H_2_1:le x_2_1 y_2_1), forall (H_2_2:le x_2_2 y_2_2), forall (H_2_3:le x_2_3 y_2_3), forall (H_3_0:le x_3_0 y_3_0), forall (H_3_1:le x_3_1 y_3_1), forall (H_3_2:le x_3_2 y_3_2), forall (H_3_3:le x_3_3 y_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))))))))) (y_0_0, ((y_0_1,(y_0_2,y_0_3)), ((y_1_0,(y_2_0,y_3_0)), (y_1_1, ((y_1_2,y_1_3), ((y_2_1,y_3_1), (y_2_2, (y_2_3, (y_3_2,y_3_3))))))))) (conj H_0_0 (conj (conj H_0_1 (conj H_0_2 H_0_3)) (conj (conj H_1_0 (conj H_2_0 H_3_0)) (conj H_1_1 (conj (conj H_1_2 H_1_3) (conj (conj H_2_1 H_3_1) (conj H_2_2 (conj H_2_3 (conj H_3_2 H_3_3))))))))) ), forall (m1 m2:matrix 3), forall (H:mat_order_large _ m1 m2), P m1 m2 H.
proof: Proof. intros . induction m1 using matrix_3_ind. induction m2 using matrix_3_ind. refine match H0 with | (conj _ (conj (conj _ (conj _ _)) (conj (conj _ (conj _ _)) (conj _ (conj (conj _ _) (conj (conj _ _) (conj _ (conj _ (conj _ _)))))) ))) => _ end. apply H. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)