// This prints the left floatting menu

### Theoremgcd.let_clause_1571

Statement

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

Main Dependencies
constant
definition
Theory

Statement

Theorem let_clause_1571 : 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 n.

Statement

theorem let_clause_1571 : \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 n.

Statement

theorem let_clause_1571 : 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)) (n).

Statement

let_clause_1571 : 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)(n)))))))

Printing for OpenTheory is not working at the moment.