idris-proofs

Commutativity of addition

Code

sym_plus : {x,y:Nat} -> x + y = y + x

Transitivity of Divisibility

Code

if b|a and b|c then c|a

on idris:

data Divb : Nat -> Nat -> Type where
  DivbAx1 : a = k*b -> a `Divb` b

theorem : a `Divb` b -> b `Divb` c -> a `Divb` c

Euler circuit theorem(in progress)

Code

Proof of the famous graph theorem about necessary and sufficient condition Eulerian graph: it has exactly two vertices of odd degree.