27. Divisibility is transitive

EasyProofFree10 points

a ∣ b means that b = a * k for some k. Prove that divisibility is transitive, working from that definition.

Solution.lean

1theorem solution (a b c : Nat) (h1 : a ∣ b) (h2 : b ∣ c) : a ∣ c := by

given

Loading editor…

Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.

a b c:Nat

h1:a ∣ b

h2:b ∣ c

⊢a ∣ c

ReadyLn 1, Col 1Lean 4

Draft saved in this browser