Proofgold Proposition

∀ x0 . ∀ x1 : ι → ι . ∀ x2 . nat_p x2 ⟶ ∀ x3 . nat_p x3 ⟶ and (ap (SNo_sqrtaux x0 x1 x2) 0 ⊆ ap (SNo_sqrtaux x0 x1 (add_nat x2 x3)) 0) (ap (SNo_sqrtaux x0 x1 x2) 1 ⊆ ap (SNo_sqrtaux x0 x1 (add_nat x2 x3)) 1)

type
prop

theory
HotG

name
SNo_sqrtaux_mon_lem

proof
PUewm..

Megalodon
SNo_sqrtaux_mon_lem

proofgold address
TMLAs..^{SNo_sqrtaux_mon_lem}

creator
27779 PrQUS../7acd6..

owner
27779 PrQUS../7acd6..

term root
be3c0..