Apply unknownprop_e9c4cec7fb327dcb17b88acdaf76daee024e49fa71834a13065f86e12e958609 with
u2,
u6,
λ x0 x1 . add_nat u51 u63 ⊆ x1 leaving 2 subgoals.
The subproof is completed by applying nat_6.
Apply unknownprop_4d619f8c0c4edc98bd8e6be92366236784a59ad7862cae98bda091f9d44c9792 with
λ x0 x1 . add_nat u51 u63 ⊆ mul_nat u2 x1.
Apply unknownprop_463ff37e0f5b1f0c9f9e5bd24ebf02eb01188a79277f3c1f714af19504beaaf2 with
u64,
λ x0 x1 . add_nat u51 u63 ⊆ x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_c00f2f77a9de84adbe221e2db786f0dbccd295ee08ec6eb8eaaf0b0a862ad5bd.
Apply Subq_tra with
add_nat u51 u63,
add_nat (add_nat u51 u63) u14,
add_nat u64 u64 leaving 2 subgoals.
Apply unknownprop_2dcf4dd8557a0ffd2a187961d1bc330ef1aae42c546555814bac26eb5e3c6d68 with
add_nat u51 u63,
u14.
The subproof is completed by applying nat_14.
Apply add_nat_SR with
add_nat u51 u63,
u13,
λ x0 x1 . x1 ⊆ add_nat u64 u64 leaving 2 subgoals.
The subproof is completed by applying nat_13.
Apply add_nat_SL with
add_nat u51 u63,
u13,
λ x0 x1 . x0 ⊆ add_nat u64 u64 leaving 3 subgoals.
Apply add_nat_p with
u51,
u63 leaving 2 subgoals.
The subproof is completed by applying unknownprop_0e4f7f5019dd72cad77d235851aaa5f40639940cef2c896847b5850af4193769.
The subproof is completed by applying unknownprop_1bb5d644e46edf4d7f31f818c9ba84409d227e8fe01f3cebddc2e7a46ab7177a.
The subproof is completed by applying nat_13.
Apply add_nat_SR with
u51,
u63,
λ x0 x1 . add_nat x0 u13 ⊆ add_nat u64 u64 leaving 2 subgoals.
The subproof is completed by applying unknownprop_1bb5d644e46edf4d7f31f818c9ba84409d227e8fe01f3cebddc2e7a46ab7177a.
Apply add_nat_com with
u51,
u64,
λ x0 x1 . add_nat x1 u13 ⊆ add_nat u64 u64 leaving 3 subgoals.
The subproof is completed by applying unknownprop_0e4f7f5019dd72cad77d235851aaa5f40639940cef2c896847b5850af4193769.
The subproof is completed by applying unknownprop_c00f2f77a9de84adbe221e2db786f0dbccd295ee08ec6eb8eaaf0b0a862ad5bd.
Apply add_nat_asso with
u64,
u51,
u13,
λ x0 x1 . x1 ⊆ add_nat u64 u64 leaving 4 subgoals.
The subproof is completed by applying unknownprop_c00f2f77a9de84adbe221e2db786f0dbccd295ee08ec6eb8eaaf0b0a862ad5bd.
The subproof is completed by applying unknownprop_0e4f7f5019dd72cad77d235851aaa5f40639940cef2c896847b5850af4193769.
The subproof is completed by applying nat_13.
Apply unknownprop_56864d25e1dc2c311308a37cde717e02009203e74fc9553fc6055512e1618e53 with
λ x0 x1 . add_nat u64 x1 ⊆ add_nat u64 u64.
The subproof is completed by applying Subq_ref with
add_nat u64 u64.