∀ m n, (gcd m n) = O ⇒ (m = O) ∧ (n = O)

Theorem gcd_O_to_eq_O : forall (m:nat.nat), forall (n:nat.nat), (logic.eq (nat.nat) (gcd m n) nat.O) -> connectives.And (logic.eq (nat.nat) m nat.O) (logic.eq (nat.nat) n nat.O).

theorem gcd_O_to_eq_O : \forall (m:nat). \forall (n:nat). ((eq) (nat) ((gcd) m n) (O) ) -> (And) ((eq) (nat) m (O) ) ((eq) (nat) n (O) ).

theorem gcd_O_to_eq_O : forall (m:nat.nat) , forall (n:nat.nat) , ((((logic.eq_) (nat.nat)) ((((gcd.gcd) ) (m)) (n))) ((nat.O) )) -> (((connectives.And) ) ((((logic.eq_) (nat.nat)) (m)) ((nat.O) ))) ((((logic.eq_) (nat.nat)) (n)) ((nat.O) )).

gcd_O_to_eq_O : LEMMA (FORALL(m:nat_sttfa_th.sttfa_nat):(FORALL(n:nat_sttfa_th.sttfa_nat):(logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](gcd_sttfa.gcd(m)(n))(nat_sttfa_th.sttfa_O) => connectives_sttfa_th.sttfa_And(logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](m)(nat_sttfa_th.sttfa_O))(logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](n)(nat_sttfa_th.sttfa_O)))))

Printing for OpenTheory is not working at the moment.