[isabelle] proof by contradiction



hello,
please can anyone help me with a hint of our to prove this codes with by
contradiction.
======================================
theory testing2 imports "~~/src/HOL/Main" begin

locale geometry =
  fixes parallel :: "'line ⇒ 'line ⇒ bool"
  and intersect :: "'line ⇒ 'line ⇒ bool"
  and angle :: "'line ⇒ 'line ⇒ nat"
  assumes axiom1: "parallel l1 l2 ⟹ angle l1 l2 = 0"
  and axiom2: "intersect l1 l2 ⟹ ¬ (angle l1 l2 = 0)"
begin

lemma parallel_not_intersect: "parallel l1 l2 ⟹ ¬ intersect l1 l2"
=================================================
thanks
Adamu


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.