(
p:
, q:
. p
p = 2qq)
P:(
Prop). (x:. P(x) 
(x':. x'<x & P(x'))) (x:. P(x))p:, q:. pp = 2qq (p':. p'<p & qq = 2p'p')| Rank | Theorem | Name |
| 13 | (p:, q:. pp = 2qq) | [two_sqr_roots] |
| cites the following: | ||
| 0 | P:(Prop). (x:. P(x) (x':. x'<x & P(x'))) (x:. P(x)) | [nat_descent] |
| 12 | p:, q:. pp = 2qq (p':. p'<p & qq = 2p'p') | [two_sqr_roots_LEMMA1] |