proposition: Lemma demo_branch : 1 = 2 \/ 2 = 3 \/ 3 = 4 \/ 4 = 4 \/ 4 = 5 \/ 5 = 6.
proof: Proof. Proof using. dup 6. branch 1 of 6. demo. branch 4 of 6. auto. branch 6 of 6. demo. branch 1. demo. branch 4. auto. branch 6. demo. Qed.
imports: TLC(LibTactics) Coq.micromega.Lia