proposition: Lemma decompose_le_matrix_3 : 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), mat_order_large 3 (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))))))))) .
proof: Proof. intros; refine (conj _ (conj (conj _ (conj _ _)) (conj (conj _ (conj _ _)) (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)