// This prints the left floatting menu
Dedukti    Load Matita      Load Coq         Load Lean        Load PVS         Load OpenTheory Load
Dedukti-jumb

Theorem

gcd.divides_gcd_r

Statement

∀ n m, (gcd n m) | m

Main Dependencies
Theory
axiom
bool.axiom_match_bool_type_falsebool.axiom_match_bool_type_truebool.match_bool_propconnectives.Iconnectives.Not_indconnectives.conjconnectives.equal_leibnizconnectives.falsityconnectives.match_And_propconnectives.match_Or_propconnectives.nmkconnectives.or_introlconnectives.or_intrordiv_mod.axiom_div_auxdiv_mod.axiom_div_aux_body_Odiv_mod.axiom_div_aux_body_Sdiv_mod.axiom_mod_auxdiv_mod.axiom_mod_aux_body_Odiv_mod.axiom_mod_aux_body_Sdiv_mod.div_mod_spec_introdiv_mod.match_div_mod_spec_propgcd.axiom_gcd_auxgcd.axiom_gcd_aux_body_Ogcd.axiom_gcd_aux_body_Sleibniz.sym_leibnizlogic.eq_indlogic.reflnat.axiom_eqbnat.axiom_eqb_body_Onat.axiom_eqb_body_Snat.axiom_filter_nat_type_Onat.axiom_filter_nat_type_Snat.axiom_lebnat.axiom_leb_body_Onat.axiom_leb_body_Snat.axiom_match_nat_type_Onat.axiom_match_nat_type_Snat.axiom_minusnat.axiom_minus_body_Onat.axiom_minus_body_Snat.axiom_plusnat.axiom_plus_body_Onat.axiom_plus_body_Snat.axiom_timesnat.axiom_times_body_Onat.axiom_times_body_Snat.le_Snat.le_indnat.le_nnat.match_nat_propnat.nat_indprimes.match_divides_propprimes.quotient
constant
bool.falsebool.match_bool_typebool.trueconnectives.Andconnectives.Falseconnectives.Notconnectives.Orconnectives.Trueconnectives.equaldiv_mod.div_auxdiv_mod.div_aux_bodydiv_mod.div_mod_specdiv_mod.mod_auxdiv_mod.mod_aux_bodygcd.gcd_auxgcd.gcd_aux_bodylogic.eqnat.Onat.Snat.eqbnat.eqb_bodynat.filter_nat_typenat.lenat.lebnat.leb_bodynat.match_nat_typenat.minusnat.minus_bodynat.plusnat.plus_bodynat.timesnat.times_bodyprimes.divides
definition
div_mod.modleibniz.leibniznat.ltprimes.dividesb
tyop
bool.boolnat.nat
Coq-Jumb
Statement

Theorem divides_gcd_r : forall (n:nat.nat), forall (m:nat.nat), primes.divides (gcd n m) m.


Matita-Jumb
Statement

theorem divides_gcd_r : \forall (n:nat). \forall (m:nat). (divides) ((gcd) n m) m.


Lean-jumb
Statement

theorem divides_gcd_r : forall (n:nat.nat) , forall (m:nat.nat) , (((primes.divides) ) ((((gcd.gcd) ) (n)) (m))) (m).


PVS-jumb
Statement

divides_gcd_r : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(m:nat_sttfa_th.sttfa_nat):primes_sttfa_th.sttfa_divides(gcd_sttfa.gcd(n)(m))(m)))


OpenTheory

Printing for OpenTheory is not working at the moment.