Proofgold Proposition

∀ x0 . odd_nat x0 ⟶ ∀ x1 . nat_p x1 ⟶ iff (odd_nat x1) (odd_nat (mul_nat x0 x1))

type
prop

theory
HotG

name
odd_nat_iff_odd_mul_nat

proof
PUWsr..

Megalodon
odd_nat_iff_odd_mul_nat

proofgold address
TMYAS..^{odd_nat_iff_odd_mul_nat}

creator
23950 Pr5Zc../f3b18..

owner
23950 Pr5Zc../f3b18..

term root
9ec89..