proposition: Lemma decompose_le_matrix_1 : 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), mat_order_large 1 (x_0_0, (x_0_1, (x_1_0,x_1_1))) (y_0_0, (y_0_1, (y_1_0, y_1_1))).
proof: Proof. intros. refine (conj _ (conj _ (conj _ _)));assumption. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)