Let x, g and m be given.
Assume Hm.
Apply nat_ind to the current goal.
We will prove SNo_sqrtaux x g m 0 ⊆ SNo_sqrtaux x g (add_nat m 0) 0 ∧ SNo_sqrtaux x g m 1 ⊆ SNo_sqrtaux x g (add_nat m 0) 1.
rewrite the current goal using add_nat_0R m (from left to right).
We will prove SNo_sqrtaux x g m 0 ⊆ SNo_sqrtaux x g m 0 ∧ SNo_sqrtaux x g m 1 ⊆ SNo_sqrtaux x g m 1.
Apply andI to the current goal.
Apply Subq_ref to the current goal.
Apply Subq_ref to the current goal.
Let n be given.
Assume Hn IH.
Apply IH to the current goal.
Assume IH0: SNo_sqrtaux x g m 0 ⊆ SNo_sqrtaux x g (add_nat m n) 0.
Assume IH1: SNo_sqrtaux x g m 1 ⊆ SNo_sqrtaux x g (add_nat m n) 1.
rewrite the current goal using add_nat_SR m n Hn (from left to right).
We will prove SNo_sqrtaux x g m 0 ⊆ SNo_sqrtaux x g (ordsucc (add_nat m n)) 0 ∧ SNo_sqrtaux x g m 1 ⊆ SNo_sqrtaux x g (ordsucc (add_nat m n)) 1.
rewrite the current goal using SNo_sqrtaux_S x g (add_nat m n) (add_nat_p m Hm n Hn) (from left to right).
rewrite the current goal using tuple_2_0_eq (from left to right).
rewrite the current goal using tuple_2_1_eq (from left to right).
Apply andI to the current goal.
We will prove SNo_sqrtaux x g m 0 ⊆ SNo_sqrtaux x g (add_nat m n) 0 ∪ SNo_sqrtauxset (SNo_sqrtaux x g (add_nat m n) 0) (SNo_sqrtaux x g (add_nat m n) 1) x.
Apply Subq_tra (SNo_sqrtaux x g m 0) (SNo_sqrtaux x g (add_nat m n) 0) (SNo_sqrtaux x g (add_nat m n) 0 ∪ SNo_sqrtauxset (SNo_sqrtaux x g (add_nat m n) 0) (SNo_sqrtaux x g (add_nat m n) 1) x) IH0 to the current goal.
Apply binunion_Subq_1 to the current goal.
We will prove SNo_sqrtaux x g m 1 ⊆ SNo_sqrtaux x g (add_nat m n) 1 ∪ SNo_sqrtauxset (SNo_sqrtaux x g (add_nat m n) 0) (SNo_sqrtaux x g (add_nat m n) 0) x ∪ SNo_sqrtauxset (SNo_sqrtaux x g (add_nat m n) 1) (SNo_sqrtaux x g (add_nat m n) 1) x.
Apply Subq_tra (SNo_sqrtaux x g m 1) (SNo_sqrtaux x g (add_nat m n) 1) (SNo_sqrtaux x g (add_nat m n) 1 ∪ SNo_sqrtauxset (SNo_sqrtaux x g (add_nat m n) 0) (SNo_sqrtaux x g (add_nat m n) 0) x ∪ SNo_sqrtauxset (SNo_sqrtaux x g (add_nat m n) 1) (SNo_sqrtaux x g (add_nat m n) 1) x) IH1 to the current goal.
Apply Subq_tra (SNo_sqrtaux x g (add_nat m n) 1) (SNo_sqrtaux x g (add_nat m n) 1 ∪ SNo_sqrtauxset (SNo_sqrtaux x g (add_nat m n) 0) (SNo_sqrtaux x g (add_nat m n) 0) x) (SNo_sqrtaux x g (add_nat m n) 1 ∪ SNo_sqrtauxset (SNo_sqrtaux x g (add_nat m n) 0) (SNo_sqrtaux x g (add_nat m n) 0) x ∪ SNo_sqrtauxset (SNo_sqrtaux x g (add_nat m n) 1) (SNo_sqrtaux x g (add_nat m n) 1) x) to the current goal.
Apply binunion_Subq_1 to the current goal.
Apply binunion_Subq_1 to the current goal.
∎