proposition: Lemma decompose_le_null_matrix_1 : forall x_0_0 x_0_1, forall x_1_0 x_1_1 , forall (P:forall (m:matrix 1), (mat_order_large 1 (null_matrix 1) m) ->Prop), forall (H: forall (H_0_0:le rO x_0_0), forall (H_0_1:le rO x_0_1), forall (H_1_0:le rO x_1_0), forall (H_1_1:le rO x_1_1), P (x_0_0,(x_0_1,(x_1_0,x_1_1))) (conj H_0_0 (conj H_0_1 (conj H_1_0 H_1_1)))), forall (H:mat_order_large _ (null_matrix 1) (x_0_0,(x_0_1,(x_1_0,x_1_1)))), P (x_0_0,(x_0_1,(x_1_0,x_1_1))) H.
proof: Proof. intros . 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)