Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H2: x0 ⊆ x1.
Apply Subq_tra with
mul_nat x0 x0,
mul_nat x0 x1,
mul_nat x1 x1 leaving 2 subgoals.
Apply unknownprop_929864532141b40b768d022d9a5eb271b4e76fb202303c61c5984df8eb73ceb2 with
x0,
x1,
x0 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H0.
Apply unknownprop_d99b106d8c3aa5eb23e015bc5d27fe6284c8a3a86f85a0911e7d46761f04ef97 with
x0,
x1,
x1 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H1.