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

Theorem let_clause_1572 : forall (m:nat.nat), forall (n:nat.nat), (nat.lt nat.O n) -> (logic.eq (nat.nat) (gcd m n) nat.O) -> (logic.eq (nat.nat) m nat.O) -> (logic.eq (nat.nat) n nat.O) -> logic.eq (nat.nat) m nat.O.

theorem let_clause_1572 : \forall (m:nat). \forall (n:nat). ((lt) (O) n) -> ((eq) (nat) ((gcd) m n) (O) ) -> ((eq) (nat) m (O) ) -> ((eq) (nat) n (O) ) -> (eq) (nat) m (O) .

theorem let_clause_1572 : forall (m:nat.nat) , forall (n:nat.nat) , ((((nat.lt_) ) ((nat.O) )) (n)) -> ((((logic.eq_) (nat.nat)) ((((gcd.gcd) ) (m)) (n))) ((nat.O) )) -> ((((logic.eq_) (nat.nat)) (m)) ((nat.O) )) -> ((((logic.eq_) (nat.nat)) (n)) ((nat.O) )) -> (((logic.eq_) (nat.nat)) (m)) ((nat.O) ).

let_clause_1572 : LEMMA (FORALL(m:nat_sttfa_th.sttfa_nat):(FORALL(n:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.lt(nat_sttfa_th.sttfa_O)(n) => (logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](gcd_sttfa.gcd(m)(n))(nat_sttfa_th.sttfa_O) => (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) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](m)(nat_sttfa_th.sttfa_O)))))))

Printing for OpenTheory is not working at the moment.