proposition: Lemma decompose_le_null_matrix_2 : 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, forall (P:forall (m:matrix 2), mat_order_large _ (null_matrix 2) m ->Prop), forall (H: forall (H_0_0:le rO x_0_0), forall (H_0_1:le rO x_0_1), forall (H_0_2:le rO x_0_2), forall (H_1_0:le rO x_1_0), forall (H_1_1:le rO x_1_1), forall (H_1_2:le rO x_1_2), forall (H_2_0:le rO x_2_0), forall (H_2_1:le rO x_2_1), forall (H_2_2:le rO 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)))))) (conj H_0_0 (conj (conj H_0_1 H_0_2) (conj (conj H_1_0 H_2_0) (conj H_1_1 (conj H_1_2 (conj H_2_1 H_2_2)))))) ), forall (H:mat_order_large _ (null_matrix 2) (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))))))), 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)))))) H.
proof: Proof. intros . refine match H0 with | (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)