dashed lines are picked by the user

figure 1

figure 2

Coq highlights particular cases : parallelogram ABDC and parallelogram ABCD