proposition: Lemma decompose_le_matrix_4 : forall x_0_0 x_0_1 x_0_2 x_0_3 x_0_4, forall x_1_0 x_1_1 x_1_2 x_1_3 x_1_4, forall x_2_0 x_2_1 x_2_2 x_2_3 x_2_4, forall x_3_0 x_3_1 x_3_2 x_3_3 x_3_4, forall x_4_0 x_4_1 x_4_2 x_4_3 x_4_4, forall y_0_0 y_0_1 y_0_2 y_0_3 y_0_4, forall y_1_0 y_1_1 y_1_2 y_1_3 y_1_4, forall y_2_0 y_2_1 y_2_2 y_2_3 y_2_4, forall y_3_0 y_3_1 y_3_2 y_3_3 y_3_4, forall y_4_0 y_4_1 y_4_2 y_4_3 y_4_4, 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_0_4:le x_0_4 y_0_4), 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_1_4:le x_1_4 y_1_4), 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_2_4:le x_2_4 y_2_4), 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), forall (H_3_4:le x_3_4 y_3_4), forall (H_4_0:le x_4_0 y_4_0), forall (H_4_1:le x_4_1 y_4_1), forall (H_4_2:le x_4_2 y_4_2), forall (H_4_3:le x_4_3 y_4_3), forall (H_4_4:le x_4_4 y_4_4), mat_order_large 4 (x_0_0, ((x_0_1, (x_0_2,(x_0_3,x_0_4))), ((x_1_0, (x_2_0,(x_3_0,x_4_0))), (x_1_1, ((x_1_2, (x_1_3,x_1_4)), ((x_2_1, (x_3_1,x_4_1)), (x_2_2, ((x_2_3,x_2_4), ((x_3_2,x_4_2), (x_3_3, (x_3_4, (x_4_3,x_4_4)))) )))))))) (y_0_0, ((y_0_1, (y_0_2,(y_0_3,y_0_4))), ((y_1_0, (y_2_0,(y_3_0,y_4_0))), (y_1_1, ((y_1_2,(y_1_3,y_1_4)), ((y_2_1, (y_3_1,y_4_1)), (y_2_2, ((y_2_3,y_2_4), ((y_3_2,y_4_2), (y_3_3, (y_3_4, (y_4_3,y_4_4))))) ))))))) .
proof: Proof. intros x_0_0 x_0_1 x_0_2 x_0_3 x_0_4 x_1_0 x_1_1 x_1_2 x_1_3 x_1_4 x_2_0 x_2_1 x_2_2. intros x_2_3 x_2_4 x_3_0 x_3_1 x_3_2 x_3_3 x_3_4 x_4_0 x_4_1 x_4_2 x_4_3 x_4_4 y_0_0. intros y_0_1 y_0_2 y_0_3 y_0_4 y_1_0 y_1_1 y_1_2 y_1_3 y_1_4 y_2_0 y_2_1 y_2_2 y_2_3. intros y_2_4 y_3_0 y_3_1 y_3_2 y_3_3 y_3_4 y_4_0 y_4_1 y_4_2 y_4_3 y_4_4 H_0_0 H_0_1. intros H_0_2 H_0_3 H_0_4 H_1_0 H_1_1 H_1_2 H_1_3 H_1_4 H_2_0 H_2_1 H_2_2 H_2_3 H_2_4. intros H_3_0 H_3_1 H_3_2 H_3_3 H_3_4 H_4_0 H_4_1 H_4_2 H_4_3 H_4_4. refine (conj _ (conj (conj _ (conj _ (conj _ _))) (conj (conj _ (conj _ (conj _ _))) (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)