proposition: Lemma decompose_le_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 y_0_0 y_0_1 y_0_2, forall y_1_0 y_1_1 y_1_2, forall y_2_0 y_2_1 y_2_2, 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_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_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), mat_order_large 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)))))) (y_0_0, ((y_0_1,y_0_2),((y_1_0,y_2_0), (y_1_1, (y_1_2, (y_2_1,y_2_2)))))).
proof: Proof. intros. refine (conj _ (conj (conj _ _) (conj (conj _ _) (conj _ (conj _ (conj _ _)))))) ;assumption. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)