proposition: Lemma un_menteur (a b c d : Z) dit: dit a = c -> dit b = d -> (d = a) \/ (b = c) -> (a = c) \/ (a = d) -> (b = c) \/ (b = d) -> a = d.
proof: Proof. Proof using. verit. Qed.
imports: SMTCoq Bool PArray Int63 List ZArith